1 /-
2 Copyright (c) 2018 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes
5 -/
6 import data.fintype
src └──────────┘
7
8 universes u v
9 open equiv function fintype finset
10 variables {α : Type u} {β : Type v}
11
12 namespace equiv.perm
13
14 def subtype_perm (f : perm α) {p : α → Prop} (h : ∀ x, p x ↔ p (f x)) : perm {x // p x} :=
15 ⟨λ x, ⟨f x, (h _).1 x.2⟩, λ x, ⟨f⁻¹ x, (h (f⁻¹ x)).2 $ by simpa using x.2⟩,
src └──────────┘ └┘
typ └──────────┘ └┘
doc └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid ┴└────┘ └┘
16 λ _, by simp, λ _, by simp⟩
id ┴
src └──┘ └──┘
typ └──┘ ┴ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st ┴ └───┘
17
18 @[simp] lemma subtype_perm_one (p : α → Prop) (h : ∀ x, p x ↔ p ((1 : perm α) x)) : @subtype_perm α 1 p h = 1 :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src ┴ └──┘ └──────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘
19 equiv.ext _ _ $ λ ⟨_, _⟩, rfl
id └───────┘ ┴ └─┘
src └───────┘ └─┘
typ └───────┘ ┴ └─┘
20
21 def of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) : perm α :=
22 ⟨λ x, if h : p x then f ⟨x, h⟩ else x, λ x, if h : p x then f⁻¹ ⟨x, h⟩ else x,
23 λ x, have h : ∀ h : p x, p (f ⟨x, h⟩), from λ h, (f ⟨x, h⟩).2,
24 by simp; split_ifs at *; simp * at *,
src └──┘ └────────────┘ └─────────┘
typ └──┘ └────────────┘ └─────────┘
doc └──┘ └────────────┘ └─────────┘
txt └──┘ └────────────┘ └─────────┘
par └──┘ └────────────┘ └─────────┘
pid └───┘ ┴┴┴└──┘
25 λ x, have h : ∀ h : p x, p (f⁻¹ ⟨x, h⟩), from λ h, (f⁻¹ ⟨x, h⟩).2,
26 by simp; split_ifs at *; simp * at *⟩
src └──┘ └────────────┘ └─────────┘
typ └──┘ └────────────┘ └─────────┘
doc └──┘ └────────────┘ └─────────┘
txt └──┘ └────────────┘ └─────────┘
par └──┘ └────────────┘ └─────────┘
pid └───┘ ┴┴┴└──┘
st └──────────────┘
27
28 instance of_subtype.is_group_hom {p : α → Prop} [decidable_pred p] : is_group_hom (@of_subtype α p _) :=
29 { map_mul := λ f g, equiv.ext _ _ $ λ x, begin
30 rw [of_subtype, of_subtype, of_subtype],
src └──┘ └┘ └┘ ┴
typ └──┘ └┘ └┘ ┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
31 by_cases h : p x,
src └───────┘ └─┘ ┴
typ └───────┘ └─┘ ┴
doc └───────┘ └─┘ ┴
txt └───────┘ └─┘ ┴
par └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
32 { have h₁ : p (f (g ⟨x, h⟩)), from (f (g ⟨x, h⟩)).2,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴ └┘ └─┘ └───┘ ┴ ┴ └┘ └───┘
typ └────────┘┴┴ ┴┴ ┴┴ ┴└┘┴└─┘ └───┘ ┴┴ ┴┴ ┴└┘┴└───┘
doc └────────┘ ┴ ┴ ┴ └┘ └─┘ └───┘ ┴ ┴ └┘ └───┘
txt └────────┘ ┴ ┴ ┴ └┘ └─┘ └───┘ ┴ ┴ └┘ └───┘
par └────────┘ ┴ ┴ ┴ └┘ └─┘ └───┘ ┴ ┴ └┘ └───┘
pid └─────┘└─┘ ┴ ┴ ┴ └┘ └─┘ └───┘ ┴ ┴ └┘ └─┘└┘
st └───────────────────────┘└─────────────────────┘└─
33 have h₂ : p (g ⟨x, h⟩), from (g ⟨x, h⟩).2,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ └┘ └┘ └───┘ ┴ └┘ └──┘
typ └────────┘┴┴ ┴┴ ┴└┘┴└┘ └───┘ ┴┴ ┴└┘┴└──┘
doc └────────┘ ┴ ┴ └┘ └┘ └───┘ ┴ └┘ └──┘
txt └────────┘ ┴ ┴ └┘ └┘ └───┘ ┴ └┘ └──┘
par └────────┘ ┴ ┴ └┘ └┘ └───┘ ┴ └┘ └──┘
pid └─────┘└─┘ ┴ ┴ └┘ └┘ └───┘ ┴ └┘ └┘└┘
st ─────────────────────────┘└─────────────────┘└─
34 simp [h, h₁, h₂] },
id ┴ └┘ └┘
src └────┘ └┘ └┘ └┘
typ └────┘┴└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ────────────────────┘└┘└
35 { simp [h] }
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ────────────┘└─
36 end }
st ──┘
37
38 @[simp] lemma of_subtype_one (p : α → Prop) [decidable_pred p] : @of_subtype α p _ 1 = 1 :=
id ┴ └────────────┘ ┴ └────────┘ ┴ ┴ ┴
src └────────────┘ └────────┘ ┴
typ ┴ └────────────┘ ┴ └────────┘ ┴ ┴ ┴
doc └──┘
39 is_group_hom.map_one of_subtype
id └──────────────────┘ └────────┘
src └──────────────────┘ └────────┘
typ └──────────────────┘ └────────┘
doc └──────────────────┘
40
41 lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=
id └──┘ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
42 by conv {to_lhs, rw [← injective.eq_iff f.injective, apply_inv_self]}
id └──────────────┘ └─────────┘ └────────────┘
src └────┘└────┘└┘└────┘└──────────────┘┴└─────────┘└┘└────────────┘┴└─
typ └────┘└────┘└┘└────┘└──────────────┘┴└─────────┘└┘└────────────┘┴└─
txt └────┘└────┘└┘└────┘ ┴ └┘ ┴└─
par └────┘└────┘└┘└────┘ ┴ └┘ ┴└─
pid ┴└─────────────┘ ┴ └┘ └┘└
st └─────┘└────┘└──────────────────────────────────┘└──────────────┘ ┴└
43
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
44 lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y :=
id └──┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
45 by rw [eq_comm, eq_inv_iff_eq, eq_comm]
id └─────┘ └───────────┘ └─────┘
src └──┘└─────┘└┘└───────────┘└┘└─────┘└─
typ └──┘└─────┘└┘└───────────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────────┘└─────────────┘└───────┘┴└
46
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
47 def disjoint (f g : perm α) := ∀ x, f x = x ∨ g x = x
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
48
49 @[symm] lemma disjoint.symm {f g : perm α} : disjoint f g → disjoint g f :=
id └──┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src └──┘ └──┘ └──────┘ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──┘ └──┘
50 by simp [disjoint, or.comm]
id └──────┘ └─────┘
src └────┘└──────┘└┘└─────┘└─
typ └────┘└──────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────
51
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
52 lemma disjoint_comm {f g : perm α} : disjoint f g ↔ disjoint g f :=
id └──┘ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──┘ └──────┘ ┴ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──┘
53 ⟨disjoint.symm, disjoint.symm⟩
id └───────────┘ └───────────┘
src └───────────┘ └───────────┘
typ └───────────┘ └───────────┘
54
55 lemma disjoint_mul_comm {f g : perm α} (h : disjoint f g) : f * g = g * f :=
id └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──────┘ ┴ ┴ ┴
typ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
56 equiv.ext _ _ $ λ x, (h x).elim
id └───────┘ ┴ ┴ ┴ └──┘
src └───────┘ └──┘
typ └───────┘ ┴ ┴ ┴ └──┘
57 (λ hf, (h (g x)).elim (λ hg, by simp [mul_apply, hf, hg])
id └┘ ┴ ┴ ┴ └──┘ └┘ └───────┘ └┘ └┘
src └──┘ └────┘└───────┘└┘ └┘ ┴
typ └┘ ┴ ┴ ┴ └──┘ └┘ └────┘└───────┘└┘└┘└┘└┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └───────────────────────┘
58 (λ hg, by simp [mul_apply, hf, g.injective hg]))
id └┘ └───────┘ └┘ └─────────┘ └┘
src └────┘└───────┘└┘ └┘└─────────┘┴ ┴
typ └┘ └────┘└───────┘└┘└┘└┘└─────────┘┴└┘┴
doc └────┘ └┘ └┘ ┴ ┴
txt └────┘ └┘ └┘ ┴ ┴
par └────┘ └┘ └┘ ┴ ┴
pid ┴┴ └┘ └┘ ┴ ┴
st └───────────────────────────────────┘
59 (λ hg, (h (f x)).elim (λ hf, by simp [mul_apply, f.injective hf, hg])
id └┘ ┴ ┴ ┴ └──┘ └┘ └───────┘ └─────────┘ └┘ └┘
src └──┘ └────┘└───────┘└┘└─────────┘┴ └┘ ┴
typ └┘ ┴ ┴ ┴ └──┘ └┘ └────┘└───────┘└┘└─────────┘┴└┘└┘└┘┴
doc └────┘ └┘ ┴ └┘ ┴
txt └────┘ └┘ ┴ └┘ ┴
par └────┘ └┘ ┴ └┘ ┴
pid ┴┴ └┘ ┴ └┘ ┴
st └───────────────────────────────────┘
60 (λ hf, by simp [mul_apply, hf, hg]))
id └┘ └───────┘ └┘ └┘
src └────┘└───────┘└┘ └┘ ┴
typ └┘ └────┘└───────┘└┘└┘└┘└┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └───────────────────────┘
61
62 @[simp] lemma disjoint_one_left (f : perm α) : disjoint 1 f := λ _, or.inl rfl
id └──┘ ┴ └──────┘ ┴ ┴ └────┘ └─┘
src └──┘ └──────┘ └────┘ └─┘
typ └──┘ ┴ └──────┘ ┴ ┴ └────┘ └─┘
doc └──┘ └──┘
63
64 @[simp] lemma disjoint_one_right (f : perm α) : disjoint f 1 := λ _, or.inr rfl
id └──┘ ┴ └──────┘ ┴ ┴ └────┘ └─┘
src └──┘ └──────┘ └────┘ └─┘
typ └──┘ ┴ └──────┘ ┴ ┴ └────┘ └─┘
doc └──┘ └──┘
65
66 lemma disjoint_mul_left {f g h : perm α} (H1 : disjoint f h) (H2 : disjoint g h) :
id └──┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src └──┘ └──────┘ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──┘
67 disjoint (f * g) h :=
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴
68 λ x, by cases H1 x; cases H2 x; simp *
id ┴ └┘ ┴ └┘ ┴
src └────┘ ┴ └────┘ ┴ └──────
typ ┴ └────┘└┘┴┴ └────┘└┘┴┴ └──────
doc └────┘ ┴ └────┘ ┴ └──────
txt └────┘ ┴ └────┘ ┴ └──────
par └────┘ ┴ └────┘ ┴ └──────
pid ┴ ┴ ┴ ┴ ┴┴└
st └───────────────────────────────
69
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
70 lemma disjoint_mul_right {f g h : perm α} (H1 : disjoint f g) (H2 : disjoint f h) :
id └──┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src └──┘ └──────┘ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──┘
71 disjoint f (g * h) :=
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴
72 by rw disjoint_comm; exact disjoint_mul_left H1.symm H2.symm
id └───────────┘ └───────────────┘ └─────┘ └─────┘
src └─┘└───────────┘ └────┘└───────────────┘┴└─────┘┴└─────┘└
typ └─┘└───────────┘ └────┘└───────────────┘┴└─────┘┴└─────┘└
doc └─┘ └────┘ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────────
73
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
74 lemma disjoint_prod_right {f : perm α} (l : list (perm α))
id └──┘ ┴ └──┘ └──┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ └──┘ └──┘ ┴
doc └──┘ └──┘
75 (h : ∀ g ∈ l, disjoint f g) : disjoint f l.prod :=
id ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴└───┘
src ┴ └──────┘ └──────┘ └───┘
typ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴└───┘
doc └───┘
76 begin
st └─────
77 induction l with g l ih,
id ┴
src └────────┘ └──────────┘
typ └────────┘┴└──────────┘
doc └────────┘ └──────────┘
txt └────────┘ └──────────┘
par └────────┘ └──────────┘
pid ┴ ┴└─────────┘
st ────────────────────────┘└─
78 { exact disjoint_one_right _ },
id └────────────────┘
src └────┘└────────────────┘└─┘
typ └────┘└────────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───┘└─────────────────────────┘└┘└
79 { rw list.prod_cons;
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────
80 exact disjoint_mul_right (h _ (list.mem_cons_self _ _))
id └────────────────┘ └────────────────┘
src └────┘└────────────────┘┴ └─┘ └────────────────┘└──────
typ └────┘└────────────────┘┴ └─┘ └────────────────┘└──────
doc └────┘ ┴ └─┘ └──────
txt └────┘ ┴ └─┘ └──────
par └────┘ ┴ └─┘ └──────
pid ┴ ┴ └─┘ └──────
st ────────────────────────────────────────────────────────────
81 (ih (λ g hg, h g (list.mem_cons_of_mem _ hg))) }
id └┘ ┴ └──────────────────┘
src ─────┘ ┴ └─────┘ ┴ ┴ └──────────────────┘└─┘ └──┘
typ ─────┘ └┘┴ └─────┘┴┴ ┴ └──────────────────┘└─┘ └──┘
doc ─────┘ ┴ └─────┘ ┴ ┴ └─┘ └──┘
txt ─────┘ ┴ └─────┘ ┴ ┴ └─┘ └──┘
par ─────┘ ┴ └─────┘ ┴ ┴ └─┘ └──┘
pid ─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘┴
st ────────────────────────────────────────────────────┘└─
82 end
st ──┘
83
84 lemma disjoint_prod_perm {l₁ l₂ : list (perm α)} (hl : l₁.pairwise disjoint)
id └──┘ └──┘ ┴ └┘└───────┘ └──────┘
src └──┘ └──┘ └───────┘ └──────┘
typ └──┘ └──┘ ┴ └┘└───────┘ └──────┘
doc └──┘ └───────┘
85 (hp : l₁ ~ l₂) : l₁.prod = l₂.prod :=
id └┘ ┴ └┘ └┘└───┘ ┴ └┘└───┘
src ┴ └───┘ ┴ └───┘
typ └┘ ┴ └┘ └┘└───┘ ┴ └┘└───┘
doc ┴ └───┘ └───┘
86 begin
st └─────
87 induction hp,
id └┘
src └────────┘
typ └────────┘└┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ─────────────┘└─
88 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
89 { rw [list.prod_cons, list.prod_cons, hp_ih (list.pairwise_cons.1 hl).2] },
id └────────────┘ └────────────┘ └───┘ └────────────────┘ └┘
src └──┘└────────────┘└┘└────────────┘└┘ ┴ └────────────────┘└─┘ └───┘
typ └──┘└────────────┘└┘└────────────┘└┘└───┘┴ └────────────────┘└─┘└┘└───┘
doc └──┘ └┘ └┘ ┴ └─┘ └───┘
txt └──┘ └┘ └┘ ┴ └─┘ └───┘
par └──┘ └┘ └┘ ┴ └─┘ └───┘
pid └┘ └┘ └┘ ┴ └─┘ └──┘┴
st ───┘└────────────────┘└──────────────┘└───────────────────────────────┘└─┘┴└┘└
90 { simp [list.prod_cons, disjoint_mul_comm, (mul_assoc _ _ _).symm, *,
id └────────────┘ └───────────────┘ └───────┘
src └────┘└────────────┘└┘└───────────────┘└┘ └───────┘└────────────────
typ └────┘└────────────┘└┘└───────────────┘└┘ └───────┘└────────────────
doc └────┘ └┘ └┘ └────────────────
txt └────┘ └┘ └┘ └────────────────
par └────┘ └┘ └┘ └────────────────
pid ┴┴ └┘ └┘ └────────────────
st ───┘└───────────────────────────────────────────────────────────────────
91 list.pairwise_cons] at * },
id └────────────────┘
src ─────┘└────────────────┘└─────┘
typ ─────┘└────────────────┘└─────┘
doc ─────┘ └─────┘
txt ─────┘ └─────┘
par ─────┘ └─────┘
pid ─────┘ ┴┴└──┘┴
st ──────────────────────────────┘└┘└
92 { rw [hp_ih_a hl, hp_ih_a_1 ((list.perm_pairwise (λ x y (h : disjoint x y), disjoint.symm h) hp_a).1 hl)] }
id └─────┘ └┘ └───────┘ └────────────────┘ └──────┘ └───────────┘ └──┘ └┘
src └──┘ ┴ └┘ ┴ └────────────────┘┴ └────────┘└──────┘┴ ┴ └─┘└───────────┘┴ └┘ └──┘ └─┘
typ └──┘└─────┘┴└┘└┘└───────┘┴ └────────────────┘┴ └────────┘└──────┘┴ ┴ └─┘└───────────┘┴ └┘└──┘└──┘└┘└─┘
doc └──┘ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ └┘ └──┘ └─┘
txt └──┘ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ └┘ └──┘ └─┘
par └──┘ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ └┘ └──┘ └─┘
pid └┘ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ └┘ └──┘ └┘┴
st ─────────────────┘└──────────────────────────────────────────────────────────────────────────────────────┘┴┴└─
93 end
st ──┘
94
95 lemma of_subtype_subtype_perm {f : perm α} {p : α → Prop} [decidable_pred p] (h₁ : ∀ x, p x ↔ p (f x))
id └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └────────────┘ ┴
typ └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
96 (h₂ : ∀ x, f x ≠ x → p x) : of_subtype (subtype_perm f h₁) = f :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └──────────┘ ┴ └┘ ┴ ┴
src ┴ └────────┘ └──────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └──────────┘ ┴ └┘ ┴ ┴
97 equiv.ext _ _ $ λ x, begin
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
st └─────
98 rw [of_subtype, subtype_perm],
id └────────┘ └──────────┘
src └──┘└────────┘└┘└──────────┘┴
typ └──┘└────────┘└┘└──────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────┘└────────────┘└──
99 by_cases hx : p x,
id ┴ ┴
src └───────┘ └─┘ ┴
typ └───────┘ └─┘┴┴┴
doc └───────┘ └─┘ ┴
txt └───────┘ └─┘ ┴
par └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────┘└─
100 { simp [hx] },
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└────────┘└┘└
101 { haveI := classical.prop_decidable,
id └──────────────────────┘
src └───────┘└──────────────────────┘
typ └───────┘└──────────────────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ────────────────────────────────────┘└─
102 simp [hx, not_not.1 (mt (h₂ x) hx)] }
id └┘ └─────┘ └┘ └┘ ┴ └┘
src └────┘ └┘└─────┘└─┘ └┘┴ ┴ └┘ └─┘
typ └────┘└┘└┘└─────┘└─┘ └┘┴ └┘┴┴└┘└┘└─┘
doc └────┘ └┘ └─┘ ┴ ┴ └┘ └─┘
txt └────┘ └┘ └─┘ ┴ ┴ └┘ └─┘
par └────┘ └┘ └─┘ ┴ ┴ └┘ └─┘
pid ┴┴ └┘ └─┘ ┴ ┴ └┘ └┘┴
st ───────────────────────────────────────┘└─
103 end
st ──┘
104
105 lemma of_subtype_apply_of_not_mem {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) {x : α} (hx : ¬ p x) :
id ┴ └────────────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └──┘ └─────┘ ┴
typ ┴ └────────────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
106 of_subtype f x = x := dif_neg hx
id └────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘
src └────────┘ ┴ └─────┘
typ └────────┘ ┴ ┴ ┴ ┴ └─────┘ └┘
107
108 lemma mem_iff_of_subtype_apply_mem {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) (x : α) :
id ┴ └────────────┘ ┴ └──┘ └─────┘ ┴ ┴
src └────────────┘ └──┘ └─────┘
typ ┴ └────────────┘ ┴ └──┘ └─────┘ ┴ ┴
doc └──┘
109 p x ↔ p ((of_subtype f : α → α) x) :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src ┴ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
110 if h : p x then by dsimp [of_subtype]; simpa [h] using (f ⟨x, h⟩).2
id └┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └┘ └─────┘└────────┘┴ └─────┘ └──────┘ ┴ └┘ └───┘
typ └┘ ┴ ┴ └─────┘└────────┘┴ └─────┘┴└──────┘ ┴┴ ┴└┘┴└───┘
doc └─────┘ ┴ └─────┘ └──────┘ ┴ └┘ └───┘
txt └─────┘ ┴ └─────┘ └──────┘ ┴ └┘ └───┘
par └─────┘ ┴ └─────┘ └──────┘ ┴ └┘ └───┘
pid ┴┴ ┴ ┴┴ ┴┴└────┘ ┴ └┘ └┘└─┘
st └────────────────────────────────────────────────┘
111 else by simp [h, of_subtype_apply_of_not_mem f h]
id ┴ └─────────────────────────┘ ┴ ┴
src └────┘ └┘└─────────────────────────┘┴ ┴ └─
typ └────┘┴└┘└─────────────────────────┘┴┴┴┴└─
doc └────┘ └┘ ┴ ┴ └─
txt └────┘ └┘ ┴ ┴ └─
par └────┘ └┘ ┴ ┴ └─
pid ┴┴ └┘ ┴ ┴ ┴└
st └──────────────────────────────────────────
112
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
113 @[simp] lemma subtype_perm_of_subtype {p : α → Prop} [decidable_pred p] (f : perm (subtype p)) :
id ┴ └────────────┘ ┴ └──┘ └─────┘ ┴
src └────────────┘ └──┘ └─────┘
typ ┴ └────────────┘ ┴ └──┘ └─────┘ ┴
doc └──┘ └──┘
114 subtype_perm (of_subtype f) (mem_iff_of_subtype_apply_mem f) = f :=
id └──────────┘ └────────┘ ┴ └──────────────────────────┘ ┴ ┴ ┴
src └──────────┘ └────────┘ └──────────────────────────┘ ┴
typ └──────────┘ └────────┘ ┴ └──────────────────────────┘ ┴ ┴ ┴
115 equiv.ext _ _ $ λ ⟨x, hx⟩, by dsimp [subtype_perm, of_subtype]; simp [show p x, from hx]
id └───────┘ ┴ └──────────┘ └────────┘ ┴ ┴ └┘
src └───────┘ └─────┘└──────────┘└┘└────────┘┴ └────┘ ┴ ┴ └─────┘ └─
typ └───────┘ ┴ └─────┘└──────────┘└┘└────────┘┴ └────┘ ┴┴┴┴└─────┘└┘└─
doc └─────┘ └┘ ┴ └────┘ ┴ ┴ └─────┘ └─
txt └─────┘ └┘ ┴ └────┘ ┴ ┴ └─────┘ └─
par └─────┘ └┘ ┴ └────┘ ┴ ┴ └─────┘ └─
pid ┴┴ └┘ ┴ ┴┴ ┴ ┴ └─────┘ ┴└
st └───────────────────────────────────────────────────────────
116
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
117 lemma pow_apply_eq_self_of_apply_eq_self {f : perm α} {x : α} (hfx : f x = x) :
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
118 ∀ n : ℕ, (f ^ n) x = x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
119 | 0 := rfl
id └─┘
src └─┘
typ └─┘
120 | (n+1) := by rw [pow_succ', mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self]
id ┴ └───────┘ └───────┘ └─┘ └────────────────────────────────┘
src ┴ └──┘└───────┘└┘└───────┘└┘ └┘ └─
typ ┴ └──┘└───────┘└┘└───────┘└┘└─┘└┘└────────────────────────────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └────────────┘└─────────┘└───┘└──────────────────────────────────┘┴└
121
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
122 lemma gpow_apply_eq_self_of_apply_eq_self {f : perm α} {x : α} (hfx : f x = x) :
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
123 ∀ n : ℤ, (f ^ n) x = x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
124 | (n : ℕ) := pow_apply_eq_self_of_apply_eq_self hfx n
id ┴ ┴ └────────────────────────────────┘ └─┘
src ┴ └────────────────────────────────┘
typ ┴ ┴ └────────────────────────────────┘ └─┘
125 | -[1+ n] := by rw [gpow_neg_succ, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]
id └──┘ ┴ └───────────┘ └───────────┘ └────────────────────────────────┘ └─┘
src └──┘ ┴ └──┘└───────────┘└┘└───────────┘└┘└────────────────────────────────┘┴ └─
typ └──┘ ┴ └──┘└───────────┘└┘└───────────┘└┘└────────────────────────────────┘┴└─┘└─
doc └──┘ └┘ └┘ ┴ └─
txt └──┘ └┘ └┘ ┴ └─
par └──┘ └┘ └┘ ┴ └─
pid └┘ └┘ └┘ ┴ ┴└
st └────────────────┘└─────────────┘└──────────────────────────────────────┘┴└
126
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
127 lemma pow_apply_eq_of_apply_apply_eq_self {f : perm α} {x : α} (hffx : f (f x) = x) :
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
128 ∀ n : ℕ, (f ^ n) x = x ∨ (f ^ n) x = f x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
129 | 0 := or.inl rfl
id └────┘ └─┘
src └────┘ └─┘
typ └────┘ └─┘
130 | (n+1) := (pow_apply_eq_of_apply_apply_eq_self n).elim
id ┴┴ └─────────────────────────────────┘ └──┘
src ┴ └──┘
typ ┴┴ └─────────────────────────────────┘ └──┘
131 (λ h, or.inr (by rw [pow_succ, mul_apply, h]))
id ┴ └────┘ └──────┘ └───────┘ ┴
src └────┘ └──┘└──────┘└┘└───────┘└┘ ┴
typ ┴ └────┘ └──┘└──────┘└┘└───────┘└┘┴┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └───────────┘└─────────┘└─┘┴
132 (λ h, or.inl (by rw [pow_succ, mul_apply, h, hffx]))
id ┴ └────┘ └──────┘ └───────┘ ┴ └──┘
src └────┘ └──┘└──────┘└┘└───────┘└┘ └┘ ┴
typ ┴ └────┘ └──┘└──────┘└┘└───────┘└┘┴└┘└──┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └───────────┘└─────────┘└─┘└────┘┴
133
134 lemma gpow_apply_eq_of_apply_apply_eq_self {f : perm α} {x : α} (hffx : f (f x) = x) :
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
135 ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
136 | (n : ℕ) := pow_apply_eq_of_apply_apply_eq_self hffx n
id ┴ ┴ └─────────────────────────────────┘ └──┘
src ┴ └─────────────────────────────────┘
typ ┴ ┴ └─────────────────────────────────┘ └──┘
137 | -[1+ n] :=
id └──┘ ┴
src └──┘ ┴
typ └──┘ ┴
138 by rw [gpow_neg_succ, inv_eq_iff_eq, ← injective.eq_iff f.injective, ← mul_apply, ← pow_succ,
id └───────────┘ └───────────┘ └──────────────┘ └─────────┘ └───────┘ └──────┘
src └──┘└───────────┘└┘└───────────┘└──┘└──────────────┘┴└─────────┘└──┘└───────┘└──┘└──────┘└─
typ └──┘└───────────┘└┘└───────────┘└──┘└──────────────┘┴└─────────┘└──┘└───────┘└──┘└──────┘└─
doc └──┘ └┘ └──┘ ┴ └──┘ └──┘ └─
txt └──┘ └┘ └──┘ ┴ └──┘ └──┘ └─
par └──┘ └┘ └──┘ ┴ └──┘ └──┘ └─
pid └┘ └┘ └──┘ ┴ └──┘ └──┘ └─
st └────────────────┘└─────────────┘└──────────────────────────────┘└───────────┘└──────────┘└─
139 eq_comm, inv_eq_iff_eq, ← mul_apply, ← pow_succ', @eq_comm _ x, or.comm];
id └─────┘ └───────────┘ └───────┘ └───────┘ └─────┘ ┴ └─────┘
src ───┘└─────┘└┘└───────────┘└──┘└───────┘└──┘└───────┘└┘ └─────┘└─┘ └┘└─────┘┴
typ ───┘└─────┘└┘└───────────┘└──┘└───────┘└──┘└───────┘└┘ └─────┘└─┘┴└┘└─────┘┴
doc ───┘ └┘ └──┘ └──┘ └┘ └─┘ └┘ ┴
txt ───┘ └┘ └──┘ └──┘ └┘ └─┘ └┘ ┴
par ───┘ └┘ └──┘ └──┘ └┘ └─┘ └┘ ┴
pid ───┘ └┘ └──┘ └──┘ └┘ └─┘ └┘ ┴
st ──────────┘└─────────────┘└───────────┘└───────────┘└────────────┘└───────┘┴└─
140 exact pow_apply_eq_of_apply_apply_eq_self hffx _
id └─────────────────────────────────┘ └──┘
src └────┘└─────────────────────────────────┘┴ └──
typ └────┘└─────────────────────────────────┘┴└──┘└──
doc └────┘ ┴ └──
txt └────┘ ┴ └──
par └────┘ ┴ └──
pid ┴ ┴ └┘└
st ───────────────────────────────────────────────────
141
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
142 variable [decidable_eq α]
id └──────────┘
src └──────────┘
typ └──────────┘
143
144 def support [fintype α] (f : perm α) := univ.filter (λ x, f x ≠ x)
id └─────┘ ┴ └──┘ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ └──┘└─────┘ ┴
typ └─────┘ ┴ └──┘ ┴ └──┘└─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──┘ └──┘└─────┘
145
146 @[simp] lemma mem_support [fintype α] {f : perm α} {x : α} : x ∈ f.support ↔ f x ≠ x :=
id └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ ┴ └──────┘ ┴ ┴
typ └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────┘ └──┘
147 by simp [support]
id └─────┘
src └────┘└─────┘└─
typ └────┘└─────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────
148
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
149 def is_swap (f : perm α) := ∃ x y, x ≠ y ∧ f = swap x y
id └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘
150
151 lemma swap_mul_eq_mul_swap (f : perm α) (x y : α) : swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y) :=
id └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└┘ ┴ ┴└┘ ┴
src └──┘ └──┘ ┴ ┴ ┴ └──┘ └┘ └┘
typ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└┘ ┴ ┴└┘ ┴
doc └──┘ └──┘ └──┘
152 equiv.ext _ _ $ λ z, begin
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
st └─────
153 simp [mul_apply, swap_apply_def],
id └───────┘ └────────────┘
src └────┘└───────┘└┘└────────────┘┴
typ └────┘└───────┘└┘└────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ─────────────────────────────────┘└─
154 split_ifs;
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ─────────────
155 simp [*, eq_inv_iff_eq] at * <|> cc
id └───────────┘
src └───────┘└───────────┘└─────┘ └─┘
typ └───────┘└───────────┘└─────┘ └─┘
doc └───────┘ └─────┘ └─┘
txt └───────┘ └─────┘ └─┘
par └───────┘ └─────┘ └─┘
pid ┴└──┘ ┴┴└──┘┴ ┴
st ─────────────────────────────────────┘
156 end
st └─┘
157
158 lemma mul_swap_eq_swap_mul (f : perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f :=
id └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴ └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
159 by rw [swap_mul_eq_mul_swap, inv_apply_self, inv_apply_self]
id └──────────────────┘ └────────────┘ └────────────┘
src └──┘└──────────────────┘└┘└────────────┘└┘└────────────┘└─
typ └──┘└──────────────────┘└┘└────────────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └───────────────────────┘└──────────────┘└──────────────┘┴└
160
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
161 @[simp] lemma swap_mul_self (i j : α) : equiv.swap i j * equiv.swap i j = 1 :=
id ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ ┴ └────────┘ ┴
typ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └──┘ └────────┘ └────────┘
162 equiv.swap_swap i j
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
163
164 /-- Multiplying a permutation with `swap i j` twice gives the original permutation.
165
166 This specialization of `swap_mul_self` is useful when using cosets of permutations.
167 -/
168 @[simp]
doc └──┘
169 lemma swap_mul_self_mul (i j : α) (σ : perm α) : equiv.swap i j * (equiv.swap i j * σ) = σ :=
id ┴ └──┘ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └────────┘ ┴ └────────┘ ┴ ┴
typ ┴ └──┘ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └────────┘ └────────┘
170 by rw [←mul_assoc (swap i j) (swap i j) σ, equiv.perm.swap_mul_self, one_mul]
id └───────┘ └──┘ ┴ ┴ ┴ └──────────────────────┘ └─────┘
src └───┘└───────┘┴ ┴ ┴ └┘ └──┘┴ ┴ └┘ └┘└──────────────────────┘└┘└─────┘└─
typ └───┘└───────┘┴ ┴ ┴ └┘ └──┘┴┴┴┴└┘┴└┘└──────────────────────┘└┘└─────┘└─
doc └───┘ ┴ ┴ ┴ └┘ └──┘┴ ┴ └┘ └┘ └┘ └─
txt └───┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └─
par └───┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └─
pid └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ ┴└
st └─────────────────────────────────────┘└────────────────────────┘└───────┘┴└
171
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
172 lemma swap_mul_eq_iff {i j : α} {σ : perm α} : swap i j * σ = σ ↔ i = j :=
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
173 ⟨(assume h, have swap_id : swap i j = 1 := mul_right_cancel (trans h (one_mul σ).symm),
id ┴ └──┘ ┴ ┴ ┴ └──────────────┘ └───┘ ┴ └─────┘ ┴ └──┘
src └──┘ ┴ └──────────────┘ └───┘ └─────┘ └──┘
typ ┴ └──┘ ┴ ┴ ┴ └──────────────┘ └───┘ ┴ └─────┘ ┴ └──┘
doc └──┘
174 by {rw [←swap_apply_right i j, swap_id], refl}),
id └──────────────┘ ┴ ┴ └─────┘
src └───┘└──────────────┘┴ ┴ └┘ ┴ └──┘
typ └───┘└──────────────┘┴┴┴┴└┘└─────┘┴ └──┘
doc └───┘ ┴ ┴ └┘ ┴ └──┘
txt └───┘ ┴ ┴ └┘ ┴ └──┘
par └───┘ ┴ ┴ └┘ ┴ └──┘
pid └─┘ ┴ ┴ └┘ ┴
st └─────────────────────────┘└───────┘└─────┘└┘
175 (assume h, by erw [h, swap_self, one_mul])⟩
id ┴ ┴ └───────┘ └─────┘
src └───┘ └┘└───────┘└┘└─────┘┴
typ ┴ └───┘┴└┘└───────┘└┘└─────┘┴
doc └───┘ └┘ └┘ ┴
txt └───┘ └┘ └┘ ┴
par └───┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └─────┘└─────────┘└───────┘┴
176
177 @[simp] lemma swap_swap_apply (i j k : α) : equiv.swap i j (equiv.swap i j k) = k :=
id ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └────────┘ ┴
typ ┴ └────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └────────┘ └────────┘
178 equiv.swap_core_swap_core k i j
id └───────────────────────┘ ┴ ┴ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴ ┴ ┴
179
180 lemma is_swap_of_subtype {p : α → Prop} [decidable_pred p]
id ┴ └────────────┘ ┴
src └────────────┘
typ ┴ └────────────┘ ┴
181 {f : perm (subtype p)} (h : is_swap f) : is_swap (of_subtype f) :=
id └──┘ └─────┘ ┴ └─────┘ ┴ └─────┘ └────────┘ ┴
src └──┘ └─────┘ └─────┘ └─────┘ └────────┘
typ └──┘ └─────┘ ┴ └─────┘ ┴ └─────┘ └────────┘ ┴
doc └──┘
182 let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h in
id └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴
183 ⟨x, y, by simp at hxy; tauto,
src └─────────┘ └───┘
typ └─────────┘ └───┘
doc └─────────┘ └───┘
txt └─────────┘ └───┘
par └─────────┘ └───┘
pid ┴└────┘
st └─────────────────┘
184 equiv.ext _ _ $ λ z, begin
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
st └─────
185 rw [hxy.2, of_subtype],
id └─┘ └────────┘
src └──┘ └──┘└────────┘┴
typ └──┘└─┘└──┘└────────┘┴
doc └──┘ └──┘ ┴
txt └──┘ └──┘ ┴
par └──┘ └──┘ ┴
pid └┘ └──┘ ┴
st ──────────┘└────────────┘└──
186 simp [swap_apply_def],
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ────────────────────────┘└─
187 split_ifs;
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ───────────────
188 cc <|> simp * at *
src └─┘ └───────────
typ └─┘ └───────────
doc └─┘ └───────────
txt └─┘ └───────────
par └─┘ └───────────
pid ┴ ┴┴┴└──┘└
st ───────────────────────
189 end⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
190
191 lemma ne_and_ne_of_swap_mul_apply_ne_self {f : perm α} {x y : α}
id └──┘ ┴ ┴
src └──┘
typ └──┘ ┴ ┴
doc └──┘
192 (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
193 begin
st └─────
194 simp only [swap_apply_def, mul_apply, injective.eq_iff f.injective] at *,
id └────────────┘ └───────┘ └──────────────┘ └─────────┘
src └─────────┘└────────────┘└┘└───────┘└┘└──────────────┘┴└─────────┘└────┘
typ └─────────┘└────────────┘└┘└───────┘└┘└──────────────┘┴└─────────┘└────┘
doc └─────────┘ └┘ └┘ ┴ └────┘
txt └─────────┘ └┘ └┘ ┴ └────┘
par └─────────┘ └┘ └┘ ┴ └────┘
pid ┴└──┘└┘ └┘ └┘ ┴ ┴┴└──┘
st ─────────────────────────────────────────────────────────────────────────┘└─
195 by_cases h : f y = x,
id ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
st ─────────────────────┘└─
196 { split; intro; simp * at * },
src └───┘ └───┘ └──────────┘
typ └───┘ └───┘ └──────────┘
doc └───┘ └───┘ └──────────┘
txt └───┘ └───┘ └──────────┘
par └───┘ └───┘ └──────────┘
pid ┴┴┴└──┘┴
st ───┘└────────────────────────┘└┘└
197 { split_ifs at hy; cc }
src └─────────────┘ └─┘
typ └─────────────┘ └─┘
doc └─────────────┘ └─┘
txt └─────────────┘ └─┘
par └─────────────┘ └─┘
pid └────┘ ┴
st ───────────────────────┘└─
198 end
st ──┘
199
200 lemma support_swap_mul_eq [fintype α] {f : perm α} {x : α}
id └─────┘ ┴ └──┘ ┴ ┴
src └─────┘ └──┘
typ └─────┘ ┴ └──┘ ┴ ┴
doc └─────┘ └──┘
201 (hffx : f (f x) ≠ x) : (swap x (f x) * f).support = f.support.erase x :=
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘└────┘ ┴
src ┴ └──┘ ┴ └─────┘ ┴ └──────┘└────┘
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘└────┘ ┴
doc └──┘ └────┘
202 have hfx : f x ≠ x, from λ hfx, by simpa [hfx] using hffx,
id ┴ ┴ ┴ ┴ └─┘ └─┘ └──┘
src ┴ └─────┘ └──────┘
typ ┴ ┴ ┴ ┴ └─┘ └─────┘└─┘└──────┘└──┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └─────────────────────┘
203 finset.ext.2 $ λ y,
id └────────┘┴ ┴
src └────────┘┴
typ └────────┘┴ ┴
204 ⟨λ hy, have hy' : (swap x (f x) * f) y ≠ y, from mem_support.1 hy,
id └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘┴ └┘
src └──┘ ┴ ┴ └─────────┘┴
typ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘┴ └┘
doc └──┘
205 mem_erase.2 ⟨λ hyx, by simp [hyx, mul_apply, *] at *,
id └───────┘┴ └─┘ └─┘ └───────┘
src └───────┘┴ └────┘ └┘└───────┘└───────┘
typ └───────┘┴ └─┘ └────┘└─┘└┘└───────┘└───────┘
doc └────┘ └┘ └───────┘
txt └────┘ └┘ └───────┘
par └────┘ └┘ └───────┘
pid ┴┴ └┘ └──┘┴└──┘
st └────────────────────────────┘
206 mem_support.2 $ λ hfy,
id └─────────┘┴ └─┘
src └─────────┘┴
typ └─────────┘┴ └─┘
207 by simp only [mul_apply, swap_apply_def, hfy] at hy';
id └───────┘ └────────────┘ └─┘
src └─────────┘└───────┘└┘└────────────┘└┘ └──────┘
typ └─────────┘└───────┘└┘└────────────┘└┘└─┘└──────┘
doc └─────────┘ └┘ └┘ └──────┘
txt └─────────┘ └┘ └┘ └──────┘
par └─────────┘ └┘ └┘ └──────┘
pid ┴└──┘└┘ └┘ └┘ ┴┴└────┘
st └───────────────────────────────────────────────────
208 split_ifs at hy'; simp * at *⟩,
src └──────────────┘ └─────────┘
typ └──────────────┘ └─────────┘
doc └──────────────┘ └─────────┘
txt └──────────────┘ └─────────┘
par └──────────────┘ └─────────┘
pid └─────┘ ┴┴┴└──┘
st ──────────────────────────────────┘
209 λ hy, by simp only [mem_erase, mem_support, swap_apply_def, mul_apply] at *;
id └┘ └───────┘ └─────────┘ └────────────┘ └───────┘
src └─────────┘└───────┘└┘└─────────┘└┘└────────────┘└┘└───────┘└────┘
typ └┘ └─────────┘└───────┘└┘└─────────┘└┘└────────────┘└┘└───────┘└────┘
doc └─────────┘ └┘ └┘ └┘ └────┘
txt └─────────┘ └┘ └┘ └┘ └────┘
par └─────────┘ └┘ └┘ └┘ └────┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴└──┘
st └────────────────────────────────────────────────────────────────────
210 intro; split_ifs at *; simp * at *⟩
src └───┘ └────────────┘ └─────────┘
typ └───┘ └────────────┘ └─────────┘
doc └───┘ └────────────┘ └─────────┘
txt └───┘ └────────────┘ └─────────┘
par └───┘ └────────────┘ └─────────┘
pid └───┘ ┴┴┴└──┘
st ─────────────────────────────────────┘
211
212 lemma card_support_swap_mul [fintype α] {f : perm α} {x : α}
id └─────┘ ┴ └──┘ ┴ ┴
src └─────┘ └──┘
typ └─────┘ ┴ └──┘ ┴ ┴
doc └─────┘ └──┘
213 (hx : f x ≠ x) : (swap x (f x) * f).support.card < f.support.card :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴└──────┘└───┘
src ┴ └──┘ ┴ └─────┘ └──┘ ┴ └──────┘└───┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴└──────┘└───┘
doc └──┘ └──┘ └───┘
214 finset.card_lt_card
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
215 ⟨λ z hz, mem_support.2 (ne_and_ne_of_swap_mul_apply_ne_self (mem_support.1 hz)).1,
id ┴ └┘ └─────────┘┴ └─────────────────────────────────┘ └─────────┘┴ └┘ ┴
src └─────────┘┴ └─────────────────────────────────┘ └─────────┘┴ ┴
typ ┴ └┘ └─────────┘┴ └─────────────────────────────────┘ └─────────┘┴ └┘ ┴
216 λ h, absurd (h (mem_support.2 hx)) (mt mem_support.1 (by simp))⟩
id ┴ └────┘ ┴ └─────────┘┴ └┘ └┘ └─────────┘┴
src └────┘ └─────────┘┴ └┘ └─────────┘┴ └──┘
typ ┴ └────┘ ┴ └─────────┘┴ └┘ └┘ └─────────┘┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
217
218 def swap_factors_aux : Π (l : list α) (f : perm α), (∀ {x}, f x ≠ x → x ∈ l) →
id ┴ └──┘ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ ┴
typ ┴ └──┘ ┴ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
219 {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g}
id ┴ └──┘ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └──┘ └──┘ └───┘ ┴ ┴ └─────┘
typ ┴ └──┘ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └──┘ └───┘
220 | [] := λ f h, ⟨[], equiv.ext _ _ $ λ x, by rw [list.prod_nil];
id └┘ ┴ ┴ └┘ └───────┘ ┴ └───────────┘
src └┘ └┘ └───────┘ └──┘└───────────┘┴
typ └┘ ┴ ┴ └┘ └───────┘ ┴ └──┘└───────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └────────────────┘┴└─
221 exact eq.symm (not_not.1 (mt h (list.not_mem_nil _))), by simp⟩
id └─────┘ └─────┘ └┘ ┴ └──────────────┘
src └────┘└─────┘┴ └─────┘└─┘ └┘┴ ┴ └──────────────┘└───┘ └──┘
typ └────┘└─────┘┴ └─────┘└─┘ └┘┴┴┴ └──────────────┘└───┘ └──┘
doc └────┘ ┴ └─┘ ┴ ┴ └───┘ └──┘
txt └────┘ ┴ └─┘ ┴ ┴ └───┘ └──┘
par └────┘ ┴ └─┘ ┴ ┴ └───┘ └──┘
pid ┴ ┴ └─┘ ┴ ┴ └───┘
st ────────────────────────────────────────────────────────┘ └───┘
222 | (x :: l) := λ f h,
id ┴ └┘ ┴ ┴ ┴
src └┘
typ ┴ └┘ ┴ ┴ ┴
223 if hfx : x = f x
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
224 then swap_factors_aux l f
id └──────────────┘ ┴
typ └──────────────┘ ┴
225 (λ y hy, list.mem_of_ne_of_mem (λ h : y = x, by simpa [h, hfx.symm] using hy) (h hy))
id ┴ └┘ └───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘
src └───────────────────┘ ┴ └─────┘ └┘ └──────┘
typ ┴ └┘ └───────────────────┘ ┴ ┴ └─────┘┴└┘└──────┘└──────┘└┘ ┴ └┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └───────────────────────────┘
226 else let m := swap_factors_aux l (swap x (f x) * f)
id └─┘ ┴ └──────────────┘ └──┘ ┴ ┴ ┴
src └──┘ ┴
typ └─┘ ┴ └──────────────┘ └──┘ ┴ ┴ ┴
doc └──┘
227 (λ y hy, have f y ≠ y ∧ y ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hy,
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────────────┘ └┘
src ┴ ┴ ┴ └─────────────────────────────────┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────────────┘ └┘
228 list.mem_of_ne_of_mem this.2 (h this.1)) in
id └───────────────────┘ └──┘┴ ┴ └──┘┴
src └───────────────────┘ ┴ ┴
typ └───────────────────┘ └──┘┴ ┴ └──┘┴
229 ⟨swap x (f x) :: m.1,
id └──┘ ┴ └┘ ┴┴
src └──┘ └┘ ┴
typ └──┘ ┴ └┘ ┴┴
doc └──┘
230 by rw [list.prod_cons, m.2.1, ← mul_assoc,
id └────────────┘ ┴ └───────┘
src └──┘└────────────┘└┘ └──────┘└───────┘└─
typ └──┘└────────────┘└┘┴└──────┘└───────┘└─
doc └──┘ └┘ └──────┘ └─
txt └──┘ └┘ └──────┘ └─
par └──┘ └┘ └──────┘ └─
pid └┘ └┘ └──────┘ └─
st └─────────────────┘└───┘└─────────────┘└─
231 mul_def (swap x (f x)), swap_swap, ← one_def, one_mul],
id └─────┘ └──┘ ┴ ┴ └───────┘ └─────┘ └─────┘
src ───┘└─────┘┴ └──┘┴ ┴ ┴ └──┘└───────┘└──┘└─────┘└┘└─────┘┴
typ ───┘└─────┘┴ └──┘┴ ┴ ┴┴┴└──┘└───────┘└──┘└─────┘└┘└─────┘┴
doc ───┘ ┴ └──┘┴ ┴ ┴ └──┘ └──┘ └┘ ┴
txt ───┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴
par ───┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴
pid ───┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴
st ─────────────────────────┘└─────────┘└─────────┘└───────┘┴
232 λ g hg, ((list.mem_cons_iff _ _ _).1 hg).elim (λ h, ⟨x, f x, hfx, h⟩) (m.2.2 _)⟩
id ┴ └┘ └───────────────┘ ┴ └┘ └──┘ ┴ ┴ └─┘ ┴ ┴┴ ┴
src └───────────────┘ ┴ └──┘ ┴ ┴
typ ┴ └┘ └───────────────┘ ┴ └┘ └──┘ ┴ ┴ └─┘ ┴ ┴┴ ┴
233
234 /-- `swap_factors` represents a permutation as a product of a list of transpositions.
235 The representation is non unique and depends on the linear order structure.
236 For types without linear order `trunc_swap_factors` can be used -/
237 def swap_factors [fintype α] [decidable_linear_order α] (f : perm α) :
id └─────┘ ┴ └────────────────────┘ ┴ └──┘ ┴
src └─────┘ └────────────────────┘ └──┘
typ └─────┘ ┴ └────────────────────┘ ┴ └──┘ ┴
doc └─────┘ └──┘
238 {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g} :=
id ┴ └──┘ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └──┘ └──┘ └───┘ ┴ ┴ └─────┘
typ ┴ └──┘ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └──┘ └───┘
239 swap_factors_aux ((@univ α _).sort (≤)) f (λ _ _, (mem_sort _).2 (mem_univ _))
id └──────────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘
src └──────────────┘ └──┘ └──┘ ┴ └──────┘ ┴ └──────┘
typ └──────────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘
doc └──┘ └──┘
240
241 def trunc_swap_factors [fintype α] (f : perm α) :
id └─────┘ ┴ └──┘ ┴
src └─────┘ └──┘
typ └─────┘ ┴ └──┘ ┴
doc └─────┘ └──┘
242 trunc {l : list (perm α) // l.prod = f ∧ ∀ g ∈ l, is_swap g} :=
id └───┘ ┴ └──┘ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └───┘ ┴ └──┘ └──┘ └───┘ ┴ ┴ └─────┘
typ └───┘ ┴ └──┘ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └───┘ └──┘ └───┘
243 quotient.rec_on_subsingleton (@univ α _).1
id └──────────────────────────┘ └──┘ ┴ ┴
src └──────────────────────────┘ └──┘ ┴
typ └──────────────────────────┘ └──┘ ┴ ┴
doc └──┘
244 (λ l h, trunc.mk (swap_factors_aux l f h))
id ┴ ┴ └──────┘ └──────────────┘ ┴ ┴ ┴
src └──────┘ └──────────────┘
typ ┴ ┴ └──────┘ └──────────────┘ ┴ ┴ ┴
doc └──────┘
245 (show ∀ x, f x ≠ x → x ∈ (@univ α _).1, from λ _ _, mem_univ _)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──────┘
src ┴ ┴ └──┘ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──────┘
doc └──┘
246
247 @[elab_as_eliminator] lemma swap_induction_on [fintype α] {P : perm α → Prop} (f : perm α) :
id └─────┘ ┴ └──┘ ┴ └──┘ ┴
src └─────┘ └──┘ └──┘
typ └─────┘ ┴ └──┘ ┴ └──┘ ┴
doc └────────────────┘ └─────┘ └──┘ └──┘
248 P 1 → (∀ f x y, x ≠ y → P f → P (swap x y * f)) → P f :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
249 begin
st └─────
250 cases trunc.out (trunc_swap_factors f) with l hl,
id └───────┘ └────────────────┘ ┴
src └────┘└───────┘┴ └────────────────┘┴ └─────────┘
typ └────┘└───────┘┴ └────────────────┘┴┴└─────────┘
doc └────┘└───────┘┴ ┴ └─────────┘
txt └────┘ ┴ ┴ └─────────┘
par └────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ ┴└────────┘
st ─────────────────────────────────────────────────┘└─
251 induction l with g l ih generalizing f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└─────────┘└─────────────┘
st ───────────────────────────────────────┘└─
252 { simp [hl.1.symm] {contextual := tt} },
id └┘ └┘
src └────┘ └───────┘ └────────────┘└┘└┘
typ └────┘└┘└───────┘ └────────────┘└┘└┘
doc └────┘ └───────┘ └────────────┘ └┘
txt └────┘ └───────┘ └────────────┘ └┘
par └────┘ └───────┘ └────────────┘ └┘
pid ┴┴ └──────┘┴ └────────────┘ ┴┴
st ───┘└──────────────────────────────────┘└┘└
253 { assume h1 hmul_swap,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─────────────────┘
st ──────────────────────┘└─
254 rcases hl.2 g (by simp) with ⟨x, y, hxy⟩,
id └┘ ┴
src └─────┘ └─┘ ┴ ┴└──┘└────────────────┘
typ └─────┘└┘└─┘┴┴ ┴└──┘└────────────────┘
doc └─────┘ └─┘ ┴ ┴└──┘└────────────────┘
txt └─────┘ └─┘ ┴ ┴└──┘└────────────────┘
par └─────┘ └─┘ ┴ ┴└──┘└────────────────┘
pid ┴ └─┘ ┴ └─────────────────────┘
st ────────────────────┘└───┘└────────────────┘└─
255 rw [← hl.1, list.prod_cons, hxy.2],
id └┘ └────────────┘ └─┘
src └────┘ └──┘└────────────┘└┘ └─┘
typ └────┘└┘└──┘└────────────┘└┘└─┘└─┘
doc └────┘ └──┘ └┘ └─┘
txt └────┘ └──┘ └┘ └─┘
par └────┘ └──┘ └┘ └─┘
pid └──┘ └──┘ └┘ └─┘
st ───────────┘└────────────────┘└───┘└────
256 exact hmul_swap _ _ _ hxy.1 (ih _ ⟨rfl, λ v hv, hl.2 _ (list.mem_cons_of_mem _ hv)⟩ h1 hmul_swap) }
id └─┘ └┘ └─┘ └┘ └──────────────────┘ └┘ └───────┘
src └────┘ └─────┘ └─┘ └─┘ └─┘└┘ └─────┘ └───┘ └──────────────────┘└─┘ └─┘ ┴ └┘
typ └────┘ └─────┘└─┘└─┘ └┘└─┘ └─┘└┘ └─────┘└┘└───┘ └──────────────────┘└─┘ └─┘└┘┴└───────┘└┘
doc └────┘ └─────┘ └─┘ └─┘ └┘ └─────┘ └───┘ └─┘ └─┘ ┴ └┘
txt └────┘ └─────┘ └─┘ └─┘ └┘ └─────┘ └───┘ └─┘ └─┘ ┴ └┘
par └────┘ └─────┘ └─┘ └─┘ └┘ └─────┘ └───┘ └─┘ └─┘ ┴ └┘
pid ┴ └─────┘ └─┘ └─┘ └┘ └─────┘ └───┘ └─┘ └─┘ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
257 end
st ──┘
258
259 lemma swap_mul_swap_mul_swap {x y z : α} (hwz: x ≠ y) (hxz : x ≠ z) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
260 swap y z * swap x y * swap y z = swap z x :=
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘ └──┘ └──┘
261 equiv.ext _ _ $ λ n, by simp only [swap_apply_def, mul_apply]; split_ifs; cc
id └───────┘ ┴ └────────────┘ └───────┘
src └───────┘ └─────────┘└────────────┘└┘└───────┘┴ └───────┘ └──
typ └───────┘ ┴ └─────────┘└────────────┘└┘└───────┘┴ └───────┘ └──
doc └─────────┘ └┘ ┴ └───────┘ └──
txt └─────────┘ └┘ ┴ └───────┘ └──
par └─────────┘ └┘ ┴ └───────┘ └──
pid ┴└──┘└┘ └┘ ┴ └
st └─────────────────────────────────────────────────────
262
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
263 lemma is_conj_swap {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : is_conj (swap w x) (swap y z) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ └─────┘ └──┘ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └──┘
264 have h : ∀ {y z : α}, y ≠ z → w ≠ z →
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
265 (swap w y * swap x z) * swap w x * (swap w y * swap x z)⁻¹ = swap y z :=
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴
src └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ └┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴
doc └──┘ └──┘ └──┘ └──┘ └──┘ └──┘
266 λ y z hyz hwz, by rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y),
id ┴ ┴ └─┘ └─┘ └─────────┘ └──────┘ └──────┘ └───────┘ └──┘ ┴ ┴
src └──┘└─────────┘└┘└──────┘└┘└──────┘└┘└───────┘┴ └──┘┴ ┴ └──
typ ┴ ┴ └─┘ └─┘ └──┘└─────────┘└┘└──────┘└┘└──────┘└┘└───────┘┴ └──┘┴┴┴┴└──
doc └──┘ └┘ └┘ └┘ ┴ └──┘┴ ┴ └──
txt └──┘ └┘ └┘ └┘ ┴ ┴ ┴ └──
par └──┘ └┘ └┘ └┘ ┴ ┴ ┴ └──
pid └┘ └┘ └┘ └┘ ┴ ┴ ┴ └──
st └──────────────┘└────────┘└────────┘└────────────────────┘└─
267 mul_assoc (swap w y), ← mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz,
id └───────┘ └──┘ ┴ ┴ └───────┘ └──┘ ┴ ┴ └────────────────────┘ └─┘ └─┘
src ───┘└───────┘┴ └──┘┴ ┴ └────┘└───────┘└─┘ └──┘┴ ┴ └─┘└────────────────────┘┴ ┴ └─
typ ───┘└───────┘┴ └──┘┴┴┴┴└────┘└───────┘└─┘ └──┘┴┴┴┴└─┘└────────────────────┘┴└─┘┴└─┘└─
doc ───┘ ┴ └──┘┴ ┴ └────┘ └─┘ └──┘┴ ┴ └─┘ ┴ ┴ └─
txt ───┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └─
par ───┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └─
pid ───┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └─
st ───────────────────────┘└─────────────────────────┘└──────────────────────────────┘└─
268 ← mul_assoc, swap_mul_swap_mul_swap hwz.symm hyz.symm],
id └───────┘ └────────────────────┘ └──────┘ └──────┘
src ─────┘└───────┘└┘└────────────────────┘┴└──────┘┴└──────┘┴
typ ─────┘└───────┘└┘└────────────────────┘┴└──────┘┴└──────┘┴
doc ─────┘ └┘ ┴ ┴ ┴
txt ─────┘ └┘ ┴ ┴ ┴
par ─────┘ └┘ ┴ ┴ ┴
pid ─────┘ └┘ ┴ ┴ ┴
st ──────────────┘└────────────────────────────────────────┘┴
269 if hwz : w = z
id └┘ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴ ┴
270 then have hwy : w ≠ y, by cc,
id ┴ ┴ ┴
src ┴ └┘
typ ┴ ┴ ┴ └┘
doc └┘
txt └┘
par └┘
st └─┘
271 ⟨swap w z * swap x y, by rw [swap_comm y z, h hyz.symm hwy]⟩
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └──────┘ └─┘
src └──┘ ┴ └──┘ └──┘└───────┘┴ ┴ └┘ ┴└──────┘┴ ┴
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘└───────┘┴┴┴┴└┘┴┴└──────┘┴└─┘┴
doc └──┘ └──┘ └──┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └──┘ ┴ ┴ └┘ ┴ ┴ ┴
par └──┘ ┴ ┴ └┘ ┴ ┴ ┴
pid └┘ ┴ ┴ └┘ ┴ ┴ ┴
st └────────────────┘└──────────────┘┴
272 else ⟨swap w y * swap x z, h hyz hwz⟩
id ┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘ └─┘
src └──┘ ┴ └──┘
typ ┴└──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘ └─┘
doc └──┘ └──┘
273
274 /-- set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a -/
275 def fin_pairs_lt (n : ℕ) : finset (Σ a : fin n, fin n) :=
id ┴ └────┘ ┴ └─┘ ┴┴ └─┘ ┴
src ┴ └────┘ ┴ └─┘ ┴ └─┘
typ ┴ └────┘ ┴ └─┘ ┴┴ └─┘ ┴
doc └────┘
276 (univ : finset (fin n)).sigma (λ a, (range a.1).attach_fin
id └──┘ └────┘ └─┘ ┴ └───┘ ┴ └───┘ ┴┴ └────────┘
src └──┘ └────┘ └─┘ └───┘ └───┘ ┴ └────────┘
typ └──┘ └────┘ └─┘ ┴ └───┘ ┴ └───┘ ┴┴ └────────┘
doc └──┘ └────┘ └───┘ └───┘
277 (λ m hm, lt_trans (mem_range.1 hm) a.2))
id ┴ └┘ └──────┘ └───────┘┴ └┘ ┴┴
src └──────┘ └───────┘┴ ┴
typ ┴ └┘ └──────┘ └───────┘┴ └┘ ┴┴
278
279 lemma mem_fin_pairs_lt {n : ℕ} {a : Σ a : fin n, fin n} :
id ┴ ┴ └─┘ ┴┴ └─┘ ┴
src ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ └─┘ ┴┴ └─┘ ┴
280 a ∈ fin_pairs_lt n ↔ a.2 < a.1 :=
id ┴ ┴ └──────────┘ ┴ ┴ ┴┴ ┴ ┴┴
src ┴ └──────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────────┘ ┴ ┴ ┴┴ ┴ ┴┴
doc └──────────┘
281 by simp [fin_pairs_lt, fin.lt_def]
id └──────────┘ └────────┘
src └────┘└──────────┘└┘└────────┘└─
typ └────┘└──────────┘└┘└────────┘└─
doc └────┘└──────────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────
282
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
283 def sign_aux {n : ℕ} (a : perm (fin n)) : units ℤ :=
id ┴ └──┘ └─┘ ┴ └───┘ ┴
src ┴ └──┘ └─┘ └───┘ ┴
typ ┴ └──┘ └─┘ ┴ └───┘ ┴
doc └──┘
284 (fin_pairs_lt n).prod (λ x, if a x.1 ≤ a x.2 then -1 else 1)
id └──────────┘ ┴ └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴
src └──────────┘ └──┘ ┴ ┴ ┴ ┴
typ └──────────┘ ┴ └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴
doc └──────────┘ └──┘
285
286 @[simp] lemma sign_aux_one (n : ℕ) : sign_aux (1 : perm (fin n)) = 1 :=
id ┴ └──────┘ └──┘ └─┘ ┴ ┴
src ┴ └──────┘ └──┘ └─┘ ┴
typ ┴ └──────┘ └──┘ └─┘ ┴ ┴
doc └──┘ └──┘
287 begin
st └─────
288 unfold sign_aux,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
289 conv { to_rhs, rw ← @finset.prod_const_one _ (units ℤ)
id └───────────────────┘ └───┘
src └─────┘└────┘└┘└───┘ └───────────────────┘└─┘ └───┘┴ └─
typ └─────┘└────┘└┘└───┘ └───────────────────┘└─┘ └───┘┴ └─
txt └─────┘└────┘└┘└───┘ └─┘ ┴ └─
par └─────┘└────┘└┘└───┘ └─┘ ┴ └─
pid ┴└─────────────┘ └─┘ ┴ └─
st ───────┘└─────┘└─────────────────────────────────────────
290 (fin_pairs_lt n) },
id └──────────┘ ┴
src ───┘ └──────────┘┴ └┘┴
typ ───┘ └──────────┘┴┴└┘┴
doc └──────────┘
txt ───┘ ┴ └┘┴
par ───┘ ┴ └┘┴
pid ───┘ ┴ └─┘
st ────────────────────┘└┘└
291 exact finset.prod_congr rfl (λ a ha, if_neg
id └───────────────┘ └─┘ └────┘
src └────┘└───────────────┘┴└─┘┴ └─────┘└────┘└
typ └────┘└───────────────┘┴└─┘┴ └─────┘└────┘└
doc └────┘ ┴ ┴ └─────┘ └
txt └────┘ ┴ ┴ └─────┘ └
par └────┘ ┴ ┴ └─────┘ └
pid ┴ ┴ ┴ └─────┘ └
st ──────────────────────────────────────────────
292 (not_le_of_gt (mem_fin_pairs_lt.1 ha)))
id └──────────┘ └──────────────┘
src ───┘ └──────────┘┴ └──────────────┘└─┘ └──┘
typ ───┘ └──────────┘┴ └──────────────┘└─┘ └──┘
doc ───┘ ┴ └─┘ └──┘
txt ───┘ ┴ └─┘ └──┘
par ───┘ ┴ └─┘ └──┘
pid ───┘ ┴ └─┘ └─┘┴
st ───────────────────────────────────────────┘
293 end
st └─┘
294
295 def sign_bij_aux {n : ℕ} (f : perm (fin n)) (a : Σ a : fin n, fin n) :
id ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴┴ └─┘ ┴
src ┴ └──┘ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴┴ └─┘ ┴
doc └──┘
296 Σ a : fin n, fin n :=
id ┴ └─┘ ┴┴ └─┘ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴┴ └─┘ ┴
297 if hxa : f a.2 < f a.1 then ⟨f a.1, f a.2⟩ else ⟨f a.2, f a.1⟩
id └┘ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴┴ ┴ ┴┴
src └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴┴ ┴ ┴┴
298
299 lemma sign_bij_aux_inj {n : ℕ} {f : perm (fin n)} : ∀ a b : Σ a : fin n, fin n,
id ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴┴ └─┘ ┴
src ┴ └──┘ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴┴ └─┘ ┴
doc └──┘
300 a ∈ fin_pairs_lt n → b ∈ fin_pairs_lt n →
id ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴
src ┴ └──────────┘ ┴ └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
301 sign_bij_aux f a = sign_bij_aux f b → a = b :=
id └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
302 λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h, begin
id ┴ ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ ┴
st └─────
303 unfold sign_bij_aux at h,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └───────────┘└───┘
st ─────────────────────────┘└─
304 rw mem_fin_pairs_lt at *,
id └──────────────┘
src └─┘└──────────────┘└───┘
typ └─┘└──────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ─────────────────────────┘└─
305 have : ¬b₁ < b₂ := not_lt_of_ge (le_of_lt hb),
id └┘ ┴ └┘ └──────────┘ └──────┘ └┘
src └─────┘ ┴┴┴ └──┘└──────────┘┴ └──────┘┴ ┴
typ └─────┘ └┘┴┴┴└┘└──┘└──────────┘┴ └──────┘┴└┘┴
doc └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
306 split_ifs at h;
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └───┘
st ──────────────────
307 simp [*, injective.eq_iff f.injective, sigma.mk.inj_eq] at *
id └──────────────┘ └─────────┘ └─────────────┘
src └───────┘└──────────────┘┴└─────────┘└┘└─────────────┘└─────┘
typ └───────┘└──────────────┘┴└─────────┘└┘└─────────────┘└─────┘
doc └───────┘ ┴ └┘ └─────┘
txt └───────┘ ┴ └┘ └─────┘
par └───────┘ ┴ └┘ └─────┘
pid ┴└──┘ ┴ └┘ ┴┴└──┘┴
st ──────────────────────────────────────────────────────────────┘
308 end
st └─┘
309
310 lemma sign_bij_aux_surj {n : ℕ} {f : perm (fin n)} : ∀ a ∈ fin_pairs_lt n,
id ┴ └──┘ └─┘ ┴ ┴ └──────────┘ ┴
src ┴ └──┘ └─┘ └──────────┘
typ ┴ └──┘ └─┘ ┴ ┴ └──────────┘ ┴
doc └──┘ └──────────┘
311 ∃ b ∈ fin_pairs_lt n, a = sign_bij_aux f b :=
id ┴ ┴ └──────────┘ ┴┴ ┴ ┴ └──────────┘ ┴ ┴
src ┴ └──────────┘ ┴ ┴ └──────────┘
typ ┴ ┴ └──────────┘ ┴┴ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
312 λ ⟨a₁, a₂⟩ ha,
id ┴└┘ └┘ └┘
typ ┴└┘ └┘ └┘
313 if hxa : f⁻¹ a₂ < f⁻¹ a₁
id └┘ ┴└┘ ┴ ┴└┘
src └┘ └┘ ┴ └┘
typ └┘ ┴└┘ ┴ ┴└┘
314 then ⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_fin_pairs_lt.2 hxa,
id ┴└┘ ┴└┘ └──────────────┘┴ └─┘
src └┘ └┘ └──────────────┘┴
typ ┴└┘ ┴└┘ └──────────────┘┴ └─┘
315 by dsimp [sign_bij_aux];
id └──────────┘
src └─────┘└──────────┘┴
typ └─────┘└──────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └──────────────────────
316 rw [apply_inv_self, apply_inv_self, dif_pos (mem_fin_pairs_lt.1 ha)]⟩
id └────────────┘ └────────────┘ └─────┘ └──────────────┘ └┘
src └──┘└────────────┘└┘└────────────┘└┘└─────┘┴ └──────────────┘└─┘ └┘
typ └──┘└────────────┘└┘└────────────┘└┘└─────┘┴ └──────────────┘└─┘└┘└┘
doc └──┘ └┘ └┘ ┴ └─┘ └┘
txt └──┘ └┘ └┘ ┴ └─┘ └┘
par └──┘ └┘ └┘ ┴ └─┘ └┘
pid └┘ └┘ └┘ ┴ └─┘ └┘
st ───────┘└────────────┘└──────────────┘└───────────────────────────────┘┴
317 else ⟨⟨f⁻¹ a₂, f⁻¹ a₁⟩, mem_fin_pairs_lt.2 $ lt_of_le_of_ne
id ┴ ┴└┘ ┴└┘ └──────────────┘┴ └────────────┘
src └┘ └┘ └──────────────┘┴ └────────────┘
typ ┴ ┴└┘ ┴└┘ └──────────────┘┴ └────────────┘
318 (le_of_not_gt hxa) $ λ h,
id └──────────┘ └─┘ ┴
src └──────────┘
typ └──────────┘ └─┘ ┴
319 by simpa [mem_fin_pairs_lt, (f⁻¹).injective h, lt_irrefl] using ha,
id └──────────────┘ ┴└┘ ┴ └───────┘ └┘
src └─────┘└──────────────┘└┘ └┘└──────────┘ └┘└───────┘└──────┘
typ └─────┘└──────────────┘└┘ ┴└┘└──────────┘┴└┘└───────┘└──────┘└┘
doc └─────┘ └┘ └──────────┘ └┘ └──────┘
txt └─────┘ └┘ └──────────┘ └┘ └──────┘
par └─────┘ └┘ └──────────┘ └┘ └──────┘
pid ┴┴ └┘ └──────────┘ └┘ ┴┴└────┘
st └──────────────────────────────────────────────────────────────┘
320 by dsimp [sign_bij_aux];
id └──────────┘
src └─────┘└──────────┘┴
typ └─────┘└──────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └──────────────────────
321 rw [apply_inv_self, apply_inv_self,
id └────────────┘ └────────────┘
src └──┘└────────────┘└┘└────────────┘└─
typ └──┘└────────────┘└┘└────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ └─
st ───────┘└────────────┘└──────────────┘└─
322 dif_neg (not_lt_of_ge (le_of_lt (mem_fin_pairs_lt.1 ha)))]⟩
id └─────┘ └──────────┘ └──────┘ └──────────────┘ └┘
src ─────┘└─────┘┴ └──────────┘┴ └──────┘┴ └──────────────┘└─┘ └──┘
typ ─────┘└─────┘┴ └──────────┘┴ └──────┘┴ └──────────────┘└─┘└┘└──┘
doc ─────┘ ┴ ┴ ┴ └─┘ └──┘
txt ─────┘ ┴ ┴ ┴ └─┘ └──┘
par ─────┘ ┴ ┴ ┴ └─┘ └──┘
pid ─────┘ ┴ ┴ ┴ └─┘ └──┘
st ──────────────────────────────────────────────────────────────┘┴
323
324 lemma sign_bij_aux_mem {n : ℕ} {f : perm (fin n)}: ∀ a : Σ a : fin n, fin n,
id ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴┴ └─┘ ┴
src ┴ └──┘ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ └──┘ └─┘ ┴ ┴ └─┘ ┴┴ └─┘ ┴
doc └──┘
325 a ∈ fin_pairs_lt n → sign_bij_aux f a ∈ fin_pairs_lt n :=
id ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴
src ┴ └──────────┘ └──────────┘ ┴ └──────────┘
typ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
326 λ ⟨a₁, a₂⟩ ha, begin
id ┴ └┘
typ ┴ └┘
st └─────
327 unfold sign_bij_aux,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ────────────────────┘└─
328 split_ifs with h,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid ┴└────┘
st ─────────────────┘└─
329 { exact mem_fin_pairs_lt.2 h },
id └──────────────┘ ┴
src └────┘└──────────────┘└─┘ ┴
typ └────┘└──────────────┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───┘└─────────────────────────┘└┘└
330 { exact mem_fin_pairs_lt.2
src └────┘ └──
typ └────┘ └──
doc └────┘ └──
txt └────┘ └──
par └────┘ └──
pid ┴ └──
st ─────────────────────────────
331 (lt_of_le_of_ne (le_of_not_gt h)
id └────────────┘ └──────────┘ ┴
src ───┘ └────────────┘┴ └──────────┘┴ └─
typ ───┘ └────────────┘┴ └──────────┘┴┴└─
doc ───┘ ┴ ┴ └─
txt ───┘ ┴ ┴ └─
par ───┘ ┴ ┴ └─
pid ───┘ ┴ ┴ └─
st ─────────────────────────────────────
332 (λ h, ne_of_lt (mem_fin_pairs_lt.1 ha) (f.injective h.symm))) }
id └──────┘ └──────────────┘ └┘ └─────────┘ └───┘
src ─────┘ └──┘└──────┘┴ └──────────────┘└─┘ └┘ └─────────┘┴ └───┘└──┘
typ ─────┘ └──┘└──────┘┴ └──────────────┘└─┘└┘└┘ └─────────┘┴ └───┘└──┘
doc ─────┘ └──┘ ┴ └─┘ └┘ ┴ └──┘
txt ─────┘ └──┘ ┴ └─┘ └┘ ┴ └──┘
par ─────┘ └──┘ ┴ └─┘ └┘ ┴ └──┘
pid ─────┘ └──┘ ┴ └─┘ └┘ ┴ └─┘┴
st ───────────────────────────────────────────────────────────────────┘└─
333 end
st ──┘
334
335 @[simp] lemma sign_aux_inv {n : ℕ} (f : perm (fin n)) : sign_aux f⁻¹ = sign_aux f :=
id ┴ └──┘ └─┘ ┴ └──────┘ ┴└┘ ┴ └──────┘ ┴
src ┴ └──┘ └─┘ └──────┘ └┘ ┴ └──────┘
typ ┴ └──┘ └─┘ ┴ └──────┘ ┴└┘ ┴ └──────┘ ┴
doc └──┘ └──┘
336 prod_bij (λ a ha, sign_bij_aux f⁻¹ a)
id └──────┘ ┴ └┘ └──────────┘ ┴└┘ ┴
src └──────┘ └──────────┘ └┘
typ └──────┘ ┴ └┘ └──────────┘ ┴└┘ ┴
337 sign_bij_aux_mem
id └──────────────┘
src └──────────────┘
typ └──────────────┘
338 (λ ⟨a, b⟩ hab, if h : f⁻¹ b < f⁻¹ a
id ┴┴ ┴ └─┘ └┘ ┴└┘ ┴ ┴└┘
src └┘ └┘ ┴ └┘
typ ┴┴ ┴ └─┘ └┘ ┴└┘ ┴ ┴└┘
339 then by rw [sign_bij_aux, dif_pos h, if_neg (not_le_of_gt h), apply_inv_self,
id └──────────┘ └─────┘ ┴ └────┘ └──────────┘ ┴ └────────────┘
src └──┘└──────────┘└┘└─────┘┴ └┘└────┘┴ └──────────┘┴ └─┘└────────────┘└─
typ └──┘└──────────┘└┘└─────┘┴┴└┘└────┘┴ └──────────┘┴┴└─┘└────────────┘└─
doc └──┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
txt └──┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
par └──┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
pid └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
st └───────────────┘└─────────┘└───────────────────────┘└──────────────┘└─
340 apply_inv_self, if_neg (not_le_of_gt $ mem_fin_pairs_lt.1 hab)]
id └────────────┘ └────┘ └──────────┘ └──────────────┘ └─┘
src ───┘└────────────┘└┘└────┘┴ └──────────┘┴ ┴└──────────────┘└─┘ └──
typ ───┘└────────────┘└┘└────┘┴ └──────────┘┴ ┴└──────────────┘└─┘└─┘└──
doc ───┘ └┘ ┴ ┴ ┴ └─┘ └──
txt ───┘ └┘ ┴ ┴ ┴ └─┘ └──
par ───┘ └┘ ┴ ┴ ┴ └─┘ └──
pid ───┘ └┘ ┴ ┴ ┴ └─┘ └┘└
st ─────────────────┘└──────────────────────────────────────────────┘┴└
341 else by rw [sign_bij_aux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self,
id └──────────┘ └────┘ └──────────┘ ┴ └─────┘ ┴ └────────────┘
src ─┘ └──┘└──────────┘└┘└────┘┴ └──────────┘┴ └─┘└─────┘┴ └┘└────────────┘└─
typ ─┘ └──┘└──────────┘└┘└────┘┴ └──────────┘┴┴└─┘└─────┘┴┴└┘└────────────┘└─
doc ─┘ └──┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─
txt ─┘ └──┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─
par ─┘ └──┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─
pid ─┘ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─
st ─┘ └───────────────┘└───────────────────────┘└─────────┘└──────────────┘└─
342 apply_inv_self, if_pos (le_of_lt $ mem_fin_pairs_lt.1 hab)])
id └────────────┘ └────┘ └──────┘ └──────────────┘ └─┘
src ───┘└────────────┘└┘└────┘┴ └──────┘┴ ┴└──────────────┘└─┘ └┘
typ ───┘└────────────┘└┘└────┘┴ └──────┘┴ ┴└──────────────┘└─┘└─┘└┘
doc ───┘ └┘ ┴ ┴ ┴ └─┘ └┘
txt ───┘ └┘ ┴ ┴ ┴ └─┘ └┘
par ───┘ └┘ ┴ ┴ ┴ └─┘ └┘
pid ───┘ └┘ ┴ ┴ ┴ └─┘ └┘
st ─────────────────┘└──────────────────────────────────────────┘┴
343 sign_bij_aux_inj
id └──────────────┘
src └──────────────┘
typ └──────────────┘
344 sign_bij_aux_surj
id └───────────────┘
src └───────────────┘
typ └───────────────┘
345
346 lemma sign_aux_mul {n : ℕ} (f g : perm (fin n)) :
id ┴ └──┘ └─┘ ┴
src ┴ └──┘ └─┘
typ ┴ └──┘ └─┘ ┴
doc └──┘
347 sign_aux (f * g) = sign_aux f * sign_aux g :=
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ ┴ └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
348 begin
st └─────
349 rw ← sign_aux_inv g,
id └──────────┘ ┴
src └───┘└──────────┘┴
typ └───┘└──────────┘┴┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ────────────────────┘└─
350 unfold sign_aux,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
351 rw ← prod_mul_distrib,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid └──┘
st ───────────────────────┘└─
352 refine prod_bij (λ a ha, sign_bij_aux g a) sign_bij_aux_mem _
id └──────┘ └──────────┘ ┴ └──────────────┘
src └─────┘└──────┘┴ └─────┘└──────────┘┴ ┴ └┘└──────────────┘└──
typ └─────┘└──────┘┴ └─────┘└──────────┘┴┴┴ └┘└──────────────┘└──
doc └─────┘ ┴ └─────┘ ┴ ┴ └┘ └──
txt └─────┘ ┴ └─────┘ ┴ ┴ └┘ └──
par └─────┘ ┴ └─────┘ ┴ ┴ └┘ └──
pid ┴ ┴ └─────┘ ┴ ┴ └┘ └──
st ────────────────────────────────────────────────────────────────
353 sign_bij_aux_inj sign_bij_aux_surj,
id └──────────────┘ └───────────────┘
src ───┘└──────────────┘┴└───────────────┘
typ ───┘└──────────────┘┴└───────────────┘
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ─────────────────────────────────────┘└─
354 rintros ⟨a, b⟩ hab,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ───────────────────┘└─
355 rw [sign_bij_aux, mul_apply, mul_apply],
id └──────────┘ └───────┘ └───────┘
src └──┘└──────────┘└┘└───────┘└┘└───────┘┴
typ └──┘└──────────┘└┘└───────┘└┘└───────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────────────────┘└─────────┘└─────────┘└──
356 rw mem_fin_pairs_lt at hab,
id └──────────────┘
src └─┘└──────────────┘└─────┘
typ └─┘└──────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────────┘└─
357 by_cases h : g b < g a,
id ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴┴┴ ┴
typ └───────┘ └─┘ ┴┴┴┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴
st ───────────────────────┘└─
358 { rw dif_pos h,
id └─────┘ ┴
src └─┘└─────┘┴
typ └─┘└─────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───┘└──────────┘└─
359 simp [not_le_of_gt hab]; congr },
id └──────────┘ └─┘
src └────┘└──────────┘┴ ┴ └────┘
typ └────┘└──────────┘┴└─┘┴ └────┘
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴ └────┘
par └────┘ ┴ ┴ └────┘
pid ┴┴ ┴ ┴ ┴
st ──────────────────────────────────┘└┘└
360 { rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos (le_of_lt hab)],
id └─────┘ ┴ └────────────┘ └────────────┘ └────┘ └──────┘ └─┘
src └──┘└─────┘┴ └┘└────────────┘└┘└────────────┘└┘└────┘┴ └──────┘┴ └┘
typ └──┘└─────┘┴┴└┘└────────────┘└┘└────────────┘└┘└────┘┴ └──────┘┴└─┘└┘
doc └──┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘
txt └──┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘
par └──┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘
pid └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘
st ────────────────┘└──────────────┘└──────────────┘└─────────────────────┘└──
361 by_cases h₁ : f (g b) ≤ f (g a),
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ └┘┴┴ ┴ ┴ ┴
typ └───────┘ └─┘ ┴ ┴┴└┘┴┴┴┴ ┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
362 { have : f (g b) ≠ f (g a),
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └┘┴┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴┴└┘┴┴┴┴ ┴┴┴┴
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────┘└──────────────────────┘└─
363 { rw [ne.def, injective.eq_iff f.injective,
id └────┘ └──────────────┘ └─────────┘
src └──┘└────┘└┘└──────────────┘┴└─────────┘└─
typ └──┘└────┘└┘└──────────────┘┴└─────────┘└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ └─
st ───────┘└────────┘└────────────────────────────┘└─
364 injective.eq_iff g.injective];
id └──────────────┘ └─────────┘
src ─────────┘└──────────────┘┴└─────────┘┴
typ ─────────┘└──────────────┘┴└─────────┘┴
doc ─────────┘ ┴ ┴
txt ─────────┘ ┴ ┴
par ─────────┘ ┴ ┴
pid ─────────┘ ┴ ┴
st ─────────────────────────────────────┘┴└─
365 exact ne_of_lt hab },
id └──────┘ └─┘
src └────┘└──────┘┴ ┴
typ └────┘└──────┘┴└─┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────┘└┘└
366 rw [if_pos h₁, if_neg (not_le_of_gt (lt_of_le_of_ne h₁ this))],
id └────┘ └┘ └────┘ └──────────┘ └────────────┘ └┘ └──┘
src └──┘└────┘┴ └┘└────┘┴ └──────────┘└┘ └────────────┘┴ ┴ └─┘
typ └──┘└────┘┴└┘└┘└────┘┴ └──────────┘└┘ └────────────┘┴└┘┴└──┘└─┘
doc └──┘ ┴ └┘ ┴ └┘ ┴ ┴ └─┘
txt └──┘ ┴ └┘ ┴ └┘ ┴ ┴ └─┘
par └──┘ ┴ └┘ ┴ └┘ ┴ ┴ └─┘
pid └┘ ┴ └┘ ┴ └┘ ┴ ┴ └─┘
st ──────────────────┘└───────────────────────────────────────────────┘└──
367 refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└┘└
368 { rw [if_neg h₁, if_pos (le_of_lt (lt_of_not_ge h₁))],
id └────┘ └┘ └────┘ └──────┘ └──────────┘ └┘
src └──┘└────┘┴ └┘└────┘┴ └──────┘┴ └──────────┘┴ └─┘
typ └──┘└────┘┴└┘└┘└────┘┴ └──────┘┴ └──────────┘┴└┘└─┘
doc └──┘ ┴ └┘ ┴ ┴ ┴ └─┘
txt └──┘ ┴ └┘ ┴ ┴ ┴ └─┘
par └──┘ ┴ └┘ ┴ ┴ ┴ └─┘
pid └┘ ┴ └┘ ┴ ┴ ┴ └─┘
st ──────────────────┘└───────────────────────────────────┘└──
369 refl } }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└───
370 end
st ──┘
371
372 instance sign_aux.is_group_hom {n : ℕ} : is_group_hom (@sign_aux n) := { map_mul := sign_aux_mul }
id ┴ └──────────┘ └──────┘ ┴ └──────────┘
src ┴ └──────────┘ └──────┘ └──────────┘
typ ┴ └──────────┘ └──────┘ ┴ └──────────┘
doc └──────────┘
373
374 private lemma sign_aux_swap_zero_one {n : ℕ} (hn : 2 ≤ n) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
375 sign_aux (swap (⟨0, lt_of_lt_of_le dec_trivial hn⟩ : fin n)
id └──────┘ └──┘ └────────────┘ └─────────┘ └┘ └─┘ ┴
src └──────┘ └──┘ └────────────┘ └─────────┘ └─┘
typ └──────┘ └──┘ └────────────┘ └─────────┘ └┘ └─┘ ┴
doc └──┘ └─────────┘
376 ⟨1, lt_of_lt_of_le dec_trivial hn⟩) = -1 :=
id └────────────┘ └─────────┘ └┘ ┴ ┴
src └────────────┘ └─────────┘ ┴ ┴
typ └────────────┘ └─────────┘ └┘ ┴ ┴
doc └─────────┘
377 let zero : fin n := ⟨0, lt_of_lt_of_le dec_trivial hn⟩ in
id └─┘ ┴ └────────────┘ └─────────┘ └┘
src └─┘ └────────────┘ └─────────┘
typ └─┘ ┴ └────────────┘ └─────────┘ └┘
doc └─────────┘
378 let one : fin n := ⟨1, lt_of_lt_of_le dec_trivial hn⟩ in
id └─┘ ┴ └────────────┘ └─────────┘ └┘
src └─┘ └────────────┘ └─────────┘
typ └─┘ ┴ └────────────┘ └─────────┘ └┘
doc └─────────┘
379 have hzo : zero < one := dec_trivial,
id └──┘ ┴ └─┘ └─────────┘
src ┴ └─────────┘
typ └──┘ ┴ └─┘ └─────────┘
doc └─────────┘
380 show _ = (finset.singleton (⟨one, zero⟩ : Σ a : fin n, fin n)).prod
id ┴ └──────────────┘ └─┘ └──┘ ┴ └─┘ ┴┴ └─┘ ┴ └──┘
src ┴ └──────────────┘ ┴ └─┘ ┴ └─┘ └──┘
typ ┴ └──────────────┘ └─┘ └──┘ ┴ └─┘ ┴┴ └─┘ ┴ └──┘
doc └──────────────┘ └──┘
381 (λ x : Σ a : fin n, fin n, if (equiv.swap zero one) x.1
id ┴ └─┘ ┴┴ └─┘ ┴ └────────┘ └──┘ └─┘ ┴┴
src ┴ └─┘ ┴ └─┘ └────────┘ ┴
typ ┴ └─┘ ┴┴ └─┘ ┴ └────────┘ └──┘ └─┘ ┴┴
doc └────────┘
382 ≤ swap zero one x.2 then (-1 : units ℤ) else 1),
id ┴ └──┘ └──┘ └─┘ ┴┴ ┴ └───┘ ┴
src ┴ └──┘ ┴ ┴ └───┘ ┴
typ ┴ └──┘ └──┘ └─┘ ┴┴ ┴ └───┘ ┴
doc └──┘
383 begin
st └─────
384 refine eq.symm (prod_subset (λ ⟨x₁, x₂⟩, by simp [mem_fin_pairs_lt, hzo] {contextual := tt})
id └─────┘ └─────────┘ └──────────────┘ └─┘ └┘
src └─────┘└─────┘┴ └─────────┘┴ └┘ └┘ └─┘ ┴└────┘└──────────────┘└┘ └┘ └────────────┘└┘┴└─
typ └─────┘└─────┘┴ └─────────┘┴ └┘ └┘ └─┘ ┴└────┘└──────────────┘└┘└─┘└┘ └────────────┘└┘┴└─
doc └─────┘ ┴ ┴ └┘ └┘ └─┘ ┴└────┘ └┘ └┘ └────────────┘ ┴└─
txt └─────┘ ┴ ┴ └┘ └┘ └─┘ ┴└────┘ └┘ └┘ └────────────┘ ┴└─
par └─────┘ ┴ ┴ └┘ └┘ └─┘ ┴└────┘ └┘ └┘ └────────────┘ ┴└─
pid ┴ ┴ ┴ └┘ └┘ └─┘ └─────┘ └┘ └┘ └────────────┘ └──
st ────────────────────────────────────────────┘└──────────────────────────────────────────────┘└─
385 (λ a ha₁ ha₂, _)),
src ───┘ └─────────────┘
typ ───┘ └─────────────┘
doc ───┘ └─────────────┘
txt ───┘ └─────────────┘
par ───┘ └─────────────┘
pid ───┘ └─────────────┘
st ────────────────────┘└─
386 rcases a with ⟨⟨a₁, ha₁⟩, ⟨a₂, ha₂⟩⟩,
id ┴
src └─────┘ └──────────────────────────┘
typ └─────┘┴└──────────────────────────┘
doc └─────┘ └──────────────────────────┘
txt └─────┘ └──────────────────────────┘
par └─────┘ └──────────────────────────┘
pid ┴ └──────────────────────────┘
st ─────────────────────────────────────┘└─
387 replace ha₁ : a₂ < a₁ := mem_fin_pairs_lt.1 ha₁,
id └┘ ┴ └┘ └──────────────┘ └─┘
src └────────────┘ ┴┴┴ └──┘└──────────────┘└─┘
typ └────────────┘└┘┴┴┴└┘└──┘└──────────────┘└─┘└─┘
doc └────────────┘ ┴ ┴ └──┘ └─┘
txt └────────────┘ ┴ ┴ └──┘ └─┘
par └────────────┘ ┴ ┴ └──┘ └─┘
pid └──┘└─┘ ┴ ┴ └──┘ └─┘
st ────────────────────────────────────────────────┘└─
388 simp only [swap_apply_def],
id └────────────┘
src └─────────┘└────────────┘┴
typ └─────────┘└────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───────────────────────────┘└─
389 have : ¬ 1 ≤ a₂ → a₂ = 0, from λ h, nat.le_zero_iff.1 (nat.le_of_lt_succ (lt_of_not_ge h)),
id ┴ ┴ └┘ ┴ └─────────────┘ └───────────────┘ └──────────┘
src └─────┘ └─┘┴┴ ┴ ┴ ┴┴└┘ └───┘ └──┘└─────────────┘└─┘ └───────────────┘┴ └──────────┘┴ └┘
typ └─────┘┴└─┘┴┴ ┴ ┴└┘┴┴└┘ └───┘ └──┘└─────────────┘└─┘ └───────────────┘┴ └──────────┘┴ └┘
doc └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘ └─┘ ┴ ┴ └┘
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘ └─┘ ┴ ┴ └┘
par └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └───┘ └──┘ └─┘ ┴ ┴ └┘
pid └───┘└┘ └─┘ ┴ ┴ ┴ ┴ ┴┴ └───┘ └──┘ └─┘ ┴ ┴ └┘
st ─────────────────────────┘└────────────────────────────────────────────────────────────────┘└─
390 have : a₁ ≤ 1 → a₁ = 0 ∨ a₁ = 1, from nat.cases_on a₁ (λ _, or.inl rfl)
id ┴ ┴ └┘ └┘ └────┘
src └─────┘ ┴ └─┘ ┴ ┴ └─┘┴┴ ┴ └┘ └───┘ ┴ ┴ └──┘└────┘┴ └─
typ └─────┘ ┴┴└─┘ ┴ ┴ └─┘┴┴└┘┴ └┘ └───┘ ┴└┘┴ └──┘└────┘┴ └─
doc └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ └───┘ ┴ ┴ └──┘ ┴ └─
txt └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ └───┘ ┴ ┴ └──┘ ┴ └─
par └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ └───┘ ┴ ┴ └──┘ ┴ └─
pid └───┘└┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ └───┘ ┴ ┴ └──┘ ┴ └─
st ────────────────────────────────┘└────────────────────────────────────────
391 (λ a₁, nat.cases_on a₁ (λ _, or.inr rfl) (λ _ h, absurd h dec_trivial)),
id └──────────┘ └────┘ └─┘ └────┘
src ───┘ └───┘└──────────┘┴ ┴ └──┘└────┘┴└─┘└┘ └────┘└────┘┴ ┴ └┘
typ ───┘ └───┘└──────────┘┴ ┴ └──┘└────┘┴└─┘└┘ └────┘└────┘┴ ┴ └┘
doc ───┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └────┘ ┴ ┴ └┘
txt ───┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └────┘ ┴ ┴ └┘
par ───┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └────┘ ┴ ┴ └┘
pid ───┘ └───┘ ┴ ┴ └──┘ ┴ └┘ └────┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────┘└─
392 split_ifs;
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ─────────────
393 simp [*, lt_irrefl, -not_lt, not_le.symm, -not_le, le_refl, fin.lt_def, fin.le_def, nat.zero_le,
id └───────┘ └─────┘ └────────┘ └────────┘ └─────────┘
src └───────┘└───────┘└─────────┘ └─────────┘└─────┘└┘└────────┘└┘└────────┘└┘└─────────┘└─
typ └───────┘└───────┘└─────────┘└─────────┘└─────────┘└─────┘└┘└────────┘└┘└────────┘└┘└─────────┘└─
doc └───────┘ └─────────┘ └─────────┘ └┘ └┘ └┘ └─
txt └───────┘ └─────────┘ └─────────┘ └┘ └┘ └┘ └─
par └───────┘ └─────────┘ └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘ └─────────┘ └─────────┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────────────────────────────────
394 zero, one, iff.intro fin.veq_of_eq fin.eq_of_veq, nat.le_zero_iff] at *,
id └──┘ └─┘ └───────┘ └───────────┘ └───────────┘ └─────────────┘
src ───┘ └┘ └┘└───────┘┴└───────────┘┴└───────────┘└┘└─────────────┘└────┘
typ ───┘└──┘└┘└─┘└┘└───────┘┴└───────────┘┴└───────────┘└┘└─────────────┘└────┘
doc ───┘ └┘ └┘ ┴ ┴ └┘ └────┘
txt ───┘ └┘ └┘ ┴ ┴ └┘ └────┘
par ───┘ └┘ └┘ ┴ ┴ └┘ └────┘
pid ───┘ └┘ └┘ ┴ ┴ └┘ ┴┴└──┘
st ──────────────────────────────────────────────────────────────────────────┘└─
395 end
st ──┘
396
397 lemma sign_aux_swap : ∀ {n : ℕ} {x y : fin n} (hxy : x ≠ y),
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
398 sign_aux (swap x y) = -1
id └──────┘ └──┘ ┴ ┴ ┴ ┴
src └──────┘ └──┘ ┴ ┴
typ └──────┘ └──┘ ┴ ┴ ┴ ┴
doc └──┘
399 | 0 := dec_trivial
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
400 | 1 := dec_trivial
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
401 | (n+2) := λ x y hxy,
id ┴┴ ┴ ┴ └─┘
src ┴
typ ┴┴ ┴ ┴ └─┘
402 have h2n : 2 ≤ n + 2 := dec_trivial,
id ┴ ┴ └─────────┘
src ┴ ┴ └─────────┘
typ ┴ ┴ └─────────┘
doc └─────────┘
403 by rw [← is_conj_iff_eq, ← sign_aux_swap_zero_one h2n];
id └────────────┘ └────────────────────┘ └─┘
src └────┘└────────────┘└──┘└────────────────────┘┴ ┴
typ └────┘└────────────┘└──┘└────────────────────┘┴└─┘┴
doc └────┘ └──┘ ┴ ┴
txt └────┘ └──┘ ┴ ┴
par └────┘ └──┘ ┴ ┴
pid └──┘ └──┘ ┴ ┴
st └───────────────────┘└────────────────────────────┘┴└─
404 exact is_group_hom.is_conj _ (is_conj_swap hxy dec_trivial)
id └──────────────────┘ └──────────┘ └─┘ └─────────┘
src └────┘└──────────────────┘└─┘ └──────────┘┴ ┴└─────────┘└─
typ └────┘└──────────────────┘└─┘ └──────────┘┴└─┘┴└─────────┘└─
doc └────┘ └─┘ ┴ ┴ └─
txt └────┘ └─┘ ┴ ┴ └─
par └────┘ └─┘ ┴ ┴ └─
pid ┴ └─┘ ┴ ┴ ┴└
st ──────────────────────────────────────────────────────────────
405
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
406 def sign_aux2 : list α → perm α → units ℤ
id └──┘ ┴ ┴ └──┘ ┴ └───┘ ┴
src └──┘ └──┘ └───┘ ┴
typ └──┘ ┴ ┴ └──┘ ┴ └───┘ ┴
doc └──┘
407 | [] f := 1
id └┘
src └┘
typ └┘
408 | (x::l) f := if x = f x then sign_aux2 l f else -sign_aux2 l (swap x (f x) * f)
id ┴└┘┴ ┴ ┴ └───────┘ ┴└───────┘ └──┘ ┴
src └┘ ┴ ┴ └──┘ ┴
typ ┴└┘┴ ┴ ┴ └───────┘ ┴└───────┘ └──┘ ┴
doc └──┘
409
410 lemma sign_aux_eq_sign_aux2 {n : ℕ} : ∀ (l : list α) (f : perm α) (e : α ≃ fin n)
id ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴
src ┴ └──┘ └──┘ ┴ └─┘
typ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴
doc └──┘ ┴
411 (h : ∀ x, f x ≠ x → x ∈ l), sign_aux ((e.symm.trans f).trans e) = sign_aux2 l f
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴└───┘└────┘ ┴ └───┘ ┴ ┴ └───────┘ ┴ ┴
src ┴ ┴ └──────┘ └───┘└────┘ └───┘ ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴└───┘└────┘ ┴ └───┘ ┴ ┴ └───────┘ ┴ ┴
412 | [] f e h := have f = 1, from equiv.ext _ _ $
id └┘ ┴ ┴ ┴ └───────┘
src └┘ ┴ └───────┘
typ └┘ ┴ ┴ ┴ └───────┘
413 λ y, not_not.1 (mt (h y) (list.not_mem_nil _)),
id ┴ └─────┘┴ └┘ ┴ └──────────────┘
src └─────┘┴ └┘ └──────────────┘
typ ┴ └─────┘┴ └┘ ┴ └──────────────┘
414 by rw [this, one_def, equiv.trans_refl, equiv.symm_trans, ← one_def,
id └──┘ └─────┘ └──────────────┘ └──────────────┘ └─────┘
src └──┘ └┘└─────┘└┘└──────────────┘└┘└──────────────┘└──┘└─────┘└─
typ └──┘└──┘└┘└─────┘└┘└──────────────┘└┘└──────────────┘└──┘└─────┘└─
doc └──┘ └┘ └┘ └┘ └──┘ └─
txt └──┘ └┘ └┘ └┘ └──┘ └─
par └──┘ └┘ └┘ └┘ └──┘ └─
pid └┘ └┘ └┘ └┘ └──┘ └─
st └───────┘└───────┘└────────────────┘└────────────────┘└─────────┘└─
415 sign_aux_one, sign_aux2]
id └──────────┘ └───────┘
src ─┘└──────────┘└┘└───────┘└┘
typ ─┘└──────────┘└┘└───────┘└┘
doc ─┘ └┘ └┘
txt ─┘ └┘ └┘
par ─┘ └┘ └┘
pid ─┘ └┘ ┴┴
st ─────────────┘└─────────┘┴┴
416 | (x::l) f e h := begin
id └┘
src └┘
typ └┘
st └─────
417 rw sign_aux2,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────┘└─
418 by_cases hfx : x = f x,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴ ┴
typ └───────┘ └─┘ ┴┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
st ───────────────────────┘└─
419 { rw if_pos hfx,
id └────┘ └─┘
src └─┘└────┘┴
typ └─┘└────┘┴└─┘
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───┘└───────────┘└─
420 exact sign_aux_eq_sign_aux2 l f _ (λ y (hy : f y ≠ y), list.mem_of_ne_of_mem
id └───────────────────┘ ┴ ┴ ┴ └───────────────────┘
src └────┘ ┴ ┴ └─┘ └───────┘ ┴ ┴┴┴ └─┘└───────────────────┘└
typ └────┘└───────────────────┘┴┴┴ └─┘ └───────┘┴┴ ┴┴┴ └─┘└───────────────────┘└
doc └────┘ ┴ ┴ └─┘ └───────┘ ┴ ┴ ┴ └─┘ └
txt └────┘ ┴ ┴ └─┘ └───────┘ ┴ ┴ ┴ └─┘ └
par └────┘ ┴ ┴ └─┘ └───────┘ ┴ ┴ ┴ └─┘ └
pid ┴ ┴ ┴ └─┘ └───────┘ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────────────────────────────────
421 (λ h : y = x, by simpa [h, hfx.symm] using hy) (h y hy) ) },
id ┴ ┴ ┴ └┘ ┴
src ─────┘ └───┘ ┴ ┴ └┘ ┴└─────┘ └┘ └──────┘ └┘ ┴ ┴ └──┘
typ ─────┘ └───┘ ┴┴┴┴└┘ ┴└─────┘┴└┘└──────┘└──────┘└┘└┘ ┴┴ ┴ └──┘
doc ─────┘ └───┘ ┴ ┴ └┘ ┴└─────┘ └┘ └──────┘ └┘ ┴ ┴ └──┘
txt ─────┘ └───┘ ┴ ┴ └┘ ┴└─────┘ └┘ └──────┘ └┘ ┴ ┴ └──┘
par ─────┘ └───┘ ┴ ┴ └┘ ┴└─────┘ └┘ └──────┘ └┘ ┴ ┴ └──┘
pid ─────┘ └───┘ ┴ ┴ └┘ └──────┘ └┘ └──────┘ └┘ ┴ ┴ └─┘┴
st ─────────────────────┘└───────────────────────────┘└───────────┘└┘└
422 { have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l,
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴ └──┘┴ ┴ ┴ └┘┴┴ └┘ ┴ ┴ ┴ ┴ ┴┴┴
typ └────────┘ └───┘┴ ┴ └──┘┴ ┴ ┴┴└┘┴┴┴└┘ ┴┴┴ ┴ ┴ ┴┴┴┴
doc └────────┘ └───┘ ┴ └──┘┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
423 from λ y hy, have f y ≠ y ∧ y ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hy,
id ┴ ┴ └─────────────────────────────────┘
src └───┘ └─────┘ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ └─────┘└─────────────────────────────────┘┴ └─
typ └───┘ └─────┘ └─┘ ┴ ┴ ┴┴┴ ┴ ┴┴└─────┘└─────────────────────────────────┘┴ └─
doc └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
txt └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
par └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
pid └───┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─
st ──────────────────────────────────────────────────────────────────────────────────────
424 list.mem_of_ne_of_mem this.2 (h _ this.1),
id └───────────────────┘ ┴
src ─────┘└───────────────────┘┴ └─┘ └─┘ └─┘
typ ─────┘└───────────────────┘┴ └─┘ ┴└─┘ └─┘
doc ─────┘ ┴ └─┘ └─┘ └─┘
txt ─────┘ ┴ └─┘ └─┘ └─┘
par ─────┘ ┴ └─┘ └─┘ └─┘
pid ─────┘ ┴ └─┘ └─┘ └─┘
st ──────────────────────────────────────────────┘└─
425 have : (e.symm.trans (swap x (f x) * f)).trans e =
src └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └
typ └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └
doc └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └
pid └───┘└┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └
st ───────────────────────────────────────────────────────
426 (swap (e x) (e (f x))) * (e.symm.trans f).trans e,
id └──┘ ┴ └──────────┘ ┴ ┴
src ─────┘ └──┘┴ ┴ └┘ ┴ ┴ └──┘ ┴ └──────────┘┴ └──────┘
typ ─────┘ └──┘┴ ┴ └┘ ┴ ┴┴└──┘ ┴ └──────────┘┴┴└──────┘┴
doc ─────┘ └──┘┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
txt ─────┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
par ─────┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
pid ─────┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
st ──────────────────────────────────────────────────────┘└─
427 from equiv.ext _ _ (λ z, by rw ← equiv.symm_trans_swap_trans; simp [mul_def]),
id └───────┘ └─────────────────────────┘ └─────┘
src └───┘└───────┘└───┘ └──┘ ┴└───┘└─────────────────────────┘└┘└────┘└─────┘┴┴
typ └───┘└───────┘└───┘ └──┘ ┴└───┘└─────────────────────────┘└┘└────┘└─────┘┴┴
doc └───┘ └───┘ └──┘ ┴└───┘ └┘└────┘ ┴┴
txt └───┘ └───┘ └──┘ ┴└───┘ └┘└────┘ ┴┴
par └───┘ └───┘ └──┘ ┴└───┘ └┘└────┘ ┴┴
pid └───┘ └───┘ └──┘ └────┘ └──────┘ └┘
st ────────────────────────────────┘└───────────────────────────────────────────────┘┴└─
428 have hefx : e x ≠ e (f x), from mt (injective.eq_iff e.injective).1 hfx,
id ┴ ┴ ┴ └┘ └──────────────┘ └─────────┘ └─┘
src └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└┘┴ └──────────────┘┴└─────────┘└──┘
typ └──────────┘ ┴ ┴ ┴┴┴ ┴┴┴┴ └───┘└┘┴ └──────────────┘┴└─────────┘└──┘└─┘
doc └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
txt └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
par └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
st ────────────────────────────┘└────────────────────────────────────────────┘└─
429 rw [if_neg hfx, ← sign_aux_eq_sign_aux2 _ _ e hy, this, sign_aux_mul, sign_aux_swap hefx],
id └────┘ └─┘ └───────────────────┘ ┴ └┘ └──┘ └──────────┘ └───────────┘ └──┘
src └──┘└────┘┴ └──┘ └───┘ ┴ └┘ └┘└──────────┘└┘└───────────┘┴ ┴
typ └──┘└────┘┴└─┘└──┘└───────────────────┘└───┘┴┴└┘└┘└──┘└┘└──────────┘└┘└───────────┘┴└──┘┴
doc └──┘ ┴ └──┘ └───┘ ┴ └┘ └┘ └┘ ┴ ┴
txt └──┘ ┴ └──┘ └───┘ ┴ └┘ └┘ └┘ ┴ ┴
par └──┘ ┴ └──┘ └───┘ ┴ └┘ └┘ └┘ ┴ ┴
pid └┘ ┴ └──┘ └───┘ ┴ └┘ └┘ └┘ ┴ ┴
st ─────────────────┘└────────────────────────────────┘└────┘└────────────┘└──────────────────┘└──
430 simp }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
431 end
st ──┘
432
433 def sign_aux3 [fintype α] (f : perm α) {s : multiset α} : (∀ x, x ∈ s) → units ℤ :=
id └─────┘ ┴ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src └─────┘ └──┘ └──────┘ ┴ └───┘ ┴
typ └─────┘ ┴ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
doc └─────┘ └──┘ └──────┘
434 quotient.hrec_on s (λ l h, sign_aux2 l f)
id └──────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src └──────────────┘ └───────┘
typ └──────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
435 (trunc.induction_on (equiv_fin α)
id └────────────────┘ └───────┘ ┴
src └────────────────┘ └───────┘
typ └────────────────┘ └───────┘ ┴
doc └───────┘
436 (λ e l₁ l₂ h, function.hfunext
id ┴ └┘ └┘ ┴ └──────────────┘
src └──────────────┘
typ ┴ └┘ └┘ ┴ └──────────────┘
437 (show (∀ x, x ∈ l₁) = ∀ x, x ∈ l₂, by simp [list.mem_of_perm h])
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └──────────────┘ ┴
src ┴ ┴ ┴ └────┘└──────────────┘┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └────┘└──────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴┴ ┴ ┴
st └────────────────────────┘
438 (λ h₁ h₂ _, by rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, h₁ _),
id └┘ └┘ ┴ └───────────────────┘ ┴ └┘
src └────┘└───────────────────┘└───┘ ┴ └────┘ └────
typ └┘ └┘ ┴ └────┘└───────────────────┘└───┘┴┴ └────┘└┘└────
doc └────┘ └───┘ ┴ └────┘ └────
txt └────┘ └───┘ ┴ └────┘ └────
par └────┘ └───┘ ┴ └────┘ └────
pid └──┘ └───┘ ┴ └────┘ └────
st └──────────────────────────────────────────────┘└─
439 ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, h₂ _)])))
id └───────────────────┘ ┴ └┘
src ─────────┘└───────────────────┘└───┘ ┴ └────┘ └──┘
typ ─────────┘└───────────────────┘└───┘┴┴ └────┘└┘└──┘
doc ─────────┘ └───┘ ┴ └────┘ └──┘
txt ─────────┘ └───┘ ┴ └────┘ └──┘
par ─────────┘ └───┘ ┴ └────┘ └──┘
pid ─────────┘ └───┘ ┴ └────┘ └──┘
st ──────────────────────────────────────────────────┘┴
440
441 lemma sign_aux3_mul_and_swap [fintype α] (f g : perm α) (s : multiset α) (hs : ∀ x, x ∈ s) :
id └─────┘ ┴ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ └──────┘ ┴
typ └─────┘ ┴ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──┘ └──────┘
442 sign_aux3 (f * g) hs = sign_aux3 f hs * sign_aux3 g hs ∧ ∀ x y, x ≠ y →
id └───────┘ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └┘ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ └───────┘ ┴ └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └┘ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
443 sign_aux3 (swap x y) hs = -1 :=
id └───────┘ └──┘ ┴ ┴ └┘ ┴ ┴
src └───────┘ └──┘ ┴ ┴
typ └───────┘ └──┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
444 let ⟨l, hl⟩ := quotient.exists_rep s in
id └─┘ └─────────────────┘ ┴
src └─────────────────┘
typ └─┘ └─────────────────┘ ┴
445 let ⟨e, _⟩ := trunc.exists_rep (equiv_fin α) in
id └─┘ └──────────────┘ └───────┘ ┴
src └──────────────┘ └───────┘
typ └─┘ └──────────────┘ └───────┘ ┴
doc └───────┘
446 begin
st └─────
447 clear _let_match _let_match,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └────────────────────┘
st ────────────────────────────┘└─
448 subst hl,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└─
449 show sign_aux2 l (f * g) = sign_aux2 l f * sign_aux2 l g ∧
id ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴┴┴ └┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
typ └───┘ ┴ ┴ ┴┴┴ └┘┴┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴ └
doc └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────
450 ∀ x y, x ≠ y → sign_aux2 l (swap x y) = -1,
id ┴ └───────┘ ┴ └──┘ ┴
src ───┘ └──┘ ┴ ┴┴┴ ┴ ┴└───────┘┴ ┴ └──┘┴ ┴ └┘ ┴┴┴
typ ───┘ └──┘ ┴ ┴┴┴ ┴ ┴└───────┘┴┴┴ └──┘┴ ┴ └┘ ┴┴┴
doc ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘┴ ┴ └┘ ┴ ┴
txt ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid ───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────┘└─
451 have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e,
id ┴ └──────────┘ ┴ ┴
src └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────────┘┴ └──────┘
typ └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴┴└──────┘ ┴ ┴ └──────────┘┴┴└──────┘┴
doc └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘
txt └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘
par └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘
pid └──────┘└─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
452 from equiv.ext _ _ (λ h, by simp [mul_apply]),
id └───────┘ └───────┘
src └───┘└───────┘└───┘ └──┘ ┴└────┘└───────┘┴┴
typ └───┘└───────┘└───┘ └──┘ ┴└────┘└───────┘┴┴
doc └───┘ └───┘ └──┘ ┴└────┘ ┴┴
txt └───┘ └───┘ └──┘ ┴└────┘ ┴┴
par └───┘ └───┘ └──┘ ┴└────┘ ┴┴
pid └───┘ └───┘ └──┘ └─────┘ └┘
st ──────────────────────────────┘└───────────────┘┴└─
453 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
454 { rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _),
id └───────────────────┘ ┴ └┘ └───────────────────┘ ┴ └┘
src └────┘└───────────────────┘└───┘ ┴ └────┘ └─────┘└───────────────────┘└───┘ ┴ └────┘ └────
typ └────┘└───────────────────┘└───┘┴┴ └────┘└┘└─────┘└───────────────────┘└───┘┴┴ └────┘└┘└────
doc └────┘ └───┘ ┴ └────┘ └─────┘ └───┘ ┴ └────┘ └────
txt └────┘ └───┘ ┴ └────┘ └─────┘ └───┘ ┴ └────┘ └────
par └────┘ └───┘ ┴ └────┘ └─────┘ └───┘ ┴ └────┘ └────
pid └──┘ └───┘ ┴ └────┘ └─────┘ └───┘ ┴ └────┘ └────
st ───┘└─────────────────────────────────────────────┘└───────────────────────────────────────────┘└─
455 ← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), hfg, sign_aux_mul] },
id └───────────────────┘ ┴ └┘ └─┘ └──────────┘
src ───────┘└───────────────────┘└───┘ ┴ └────┘ └───┘ └┘└──────────┘└┘
typ ───────┘└───────────────────┘└───┘┴┴ └────┘└┘└───┘└─┘└┘└──────────┘└┘
doc ───────┘ └───┘ ┴ └────┘ └───┘ └┘ └┘
txt ───────┘ └───┘ ┴ └────┘ └───┘ └┘ └┘
par ───────┘ └───┘ ┴ └────┘ └───┘ └┘ └┘
pid ───────┘ └───┘ ┴ └────┘ └───┘ └┘ ┴┴
st ────────────────────────────────────────────────┘└───┘└────────────┘┴┴└┘└
456 { assume x y hxy,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ─────────────────┘└─
457 have hexy : e x ≠ e y, from mt (injective.eq_iff e.injective).1 hxy,
id ┴ ┴ ┴ └┘ └──────────────┘ └─────────┘ └─┘
src └──────────┘ ┴ ┴ ┴ ┴ └───┘└┘┴ └──────────────┘┴└─────────┘└──┘
typ └──────────┘ ┴┴┴ ┴┴┴┴ └───┘└┘┴ └──────────────┘┴└─────────┘└──┘└─┘
doc └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
txt └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
par └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘
st ────────────────────────┘└────────────────────────────────────────────┘└─
458 rw [← sign_aux_eq_sign_aux2 _ _ e (λ _ _, hs _), equiv.symm_trans_swap_trans, sign_aux_swap hexy] }
id └───────────────────┘ ┴ └┘ └─────────────────────────┘ └───────────┘ └──┘
src └────┘└───────────────────┘└───┘ ┴ └────┘ └───┘└─────────────────────────┘└┘└───────────┘┴ └┘
typ └────┘└───────────────────┘└───┘┴┴ └────┘└┘└───┘└─────────────────────────┘└┘└───────────┘┴└──┘└┘
doc └────┘ └───┘ ┴ └────┘ └───┘ └┘ ┴ └┘
txt └────┘ └───┘ ┴ └────┘ └───┘ └┘ ┴ └┘
par └────┘ └───┘ ┴ └────┘ └───┘ └┘ ┴ └┘
pid └──┘ └───┘ ┴ └────┘ └───┘ └┘ ┴ ┴┴
st ──────────────────────────────────────────────────┘└───────────────────────────┘└──────────────────┘┴┴└─
459 end
st ──┘
460
461 /-- `sign` of a permutation returns the signature or parity of a permutation, `1` for even
462 permutations, `-1` for odd permutations. It is the unique surjective group homomorphism from
463 `perm α` to the group with two elements.-/
464 def sign [fintype α] (f : perm α) := sign_aux3 f mem_univ
id └─────┘ ┴ └──┘ ┴ └───────┘ ┴ └──────┘
src └─────┘ └──┘ └───────┘ └──────┘
typ └─────┘ ┴ └──┘ ┴ └───────┘ ┴ └──────┘
doc └─────┘ └──┘
465
466 instance sign.is_group_hom [fintype α] : is_group_hom (@sign α _ _) :=
id └─────┘ ┴ └──────────┘ └──┘ ┴
src └─────┘ └──────────┘ └──┘
typ └─────┘ ┴ └──────────┘ └──┘ ┴
doc └─────┘ └──────────┘ └──┘
467 { map_mul := λ f g, (sign_aux3_mul_and_swap f g _ mem_univ).1 }
id ┴ ┴ └────────────────────┘ ┴ ┴ └──────┘ ┴
src └────────────────────┘ └──────┘ ┴
typ ┴ ┴ └────────────────────┘ ┴ ┴ └──────┘ ┴
468
469 section sign
470
471 variable [fintype α]
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
472
473 @[simp] lemma sign_mul (f g : perm α) : sign (f * g) = sign f * sign g :=
id └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └──┘ └──┘ ┴ ┴ └──┘ ┴ └──┘
typ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘ └──┘ └──┘
474 is_mul_hom.map_mul sign _ _
id └────────────────┘ └──┘
src └────────────────┘ └──┘
typ └────────────────┘ └──┘
doc └──┘
475
476 @[simp] lemma sign_one : (sign (1 : perm α)) = 1 :=
id └──┘ └──┘ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ └──┘ ┴ ┴
doc └──┘ └──┘ └──┘
477 is_group_hom.map_one sign
id └──────────────────┘ └──┘
src └──────────────────┘ └──┘
typ └──────────────────┘ └──┘
doc └──────────────────┘ └──┘
478
479 @[simp] lemma sign_refl : sign (equiv.refl α) = 1 :=
id └──┘ └────────┘ ┴ ┴
src └──┘ └────────┘ ┴
typ └──┘ └────────┘ ┴ ┴
doc └──┘ └──┘
480 is_group_hom.map_one sign
id └──────────────────┘ └──┘
src └──────────────────┘ └──┘
typ └──────────────────┘ └──┘
doc └──────────────────┘ └──┘
481
482 @[simp] lemma sign_inv (f : perm α) : sign f⁻¹ = sign f :=
id └──┘ ┴ └──┘ ┴└┘ ┴ └──┘ ┴
src └──┘ └──┘ └┘ ┴ └──┘
typ └──┘ ┴ └──┘ ┴└┘ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘ └──┘
483 by rw [is_group_hom.map_inv sign, int.units_inv_eq_self]; apply_instance
id └──────────────────┘ └──┘ └───────────────────┘
src └──┘└──────────────────┘┴└──┘└┘└───────────────────┘┴ └──────────────
typ └──┘└──────────────────┘┴└──┘└┘└───────────────────┘┴ └──────────────
doc └──┘└──────────────────┘┴└──┘└┘ ┴ └──────────────
txt └──┘ ┴ └┘ ┴ └──────────────
par └──┘ ┴ └┘ ┴ └──────────────
pid └┘ ┴ └┘ ┴ └
st └────────────────────────────┘└─────────────────────┘┴└────────────────
484
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
485 lemma sign_swap {x y : α} (h : x ≠ y) : sign (swap x y) = -1 :=
id ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴
src ┴ └──┘ └──┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘
486 (sign_aux3_mul_and_swap 1 1 _ mem_univ).2 x y h
id └────────────────────┘ └──────┘ ┴ ┴ ┴ ┴
src └────────────────────┘ └──────┘ ┴
typ └────────────────────┘ └──────┘ ┴ ┴ ┴ ┴
487
488 @[simp] lemma sign_swap' {x y : α} :
id ┴
typ ┴
doc └──┘
489 (swap x y).sign = if x = y then 1 else -1 :=
id └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
490 if H : x = y then by simp [H, swap_self] else
id └┘ ┴ ┴ ┴ ┴ └───────┘
src └┘ ┴ └────┘ └┘└───────┘└┘
typ └┘ ┴ ┴ ┴ └────┘┴└┘└───────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └───────────────────┘
491 by simp [sign_swap H, H]
id └───────┘ ┴ ┴
src └────┘└───────┘┴ └┘ └─
typ └────┘└───────┘┴┴└┘┴└─
doc └────┘ ┴ └┘ └─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid ┴┴ ┴ └┘ ┴└
st └──────────────────────
492
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
493 lemma sign_eq_of_is_swap {f : perm α} (h : is_swap f) : sign f = -1 :=
id └──┘ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴
src └──┘ └─────┘ └──┘ ┴ ┴
typ └──┘ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
494 let ⟨x, y, hxy⟩ := h in hxy.2.symm ▸ sign_swap hxy.1
id └─┘ └─┘ ┴ ┴ └──┘ ┴ └───────┘ ┴
src ┴ └──┘ ┴ └───────┘ ┴
typ └─┘ └─┘ ┴ ┴ └──┘ ┴ └───────┘ ┴
495
496 lemma sign_aux3_symm_trans_trans [decidable_eq β] [fintype β] (f : perm α)
id └──────────┘ ┴ └─────┘ ┴ └──┘ ┴
src └──────────┘ └─────┘ └──┘
typ └──────────┘ ┴ └─────┘ ┴ └──┘ ┴
doc └─────┘ └──┘
497 (e : α ≃ β) {s : multiset α} {t : multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
id ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ └──────┘ ┴ ┴
typ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └──────┘ └──────┘
498 sign_aux3 ((e.symm.trans f).trans e) ht = sign_aux3 f hs :=
id └───────┘ ┴└───┘└────┘ ┴ └───┘ ┴ └┘ ┴ └───────┘ ┴ └┘
src └───────┘ └───┘└────┘ └───┘ ┴ └───────┘
typ └───────┘ ┴└───┘└────┘ ┴ └───┘ ┴ └┘ ┴ └───────┘ ┴ └┘
499 quotient.induction_on₂ t s
id └────────────────────┘ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴
500 (λ l₁ l₂ h₁ h₂, show sign_aux2 _ _ = sign_aux2 _ _,
id └┘ └┘ └┘ └┘ └───────┘ ┴ └───────┘
src └───────┘ ┴ └───────┘
typ └┘ └┘ └┘ └┘ └───────┘ ┴ └───────┘
501 from let n := trunc.out (equiv_fin β) in
id ┴ └───────┘ └───────┘ ┴
src └───────┘ └───────┘
typ ┴ └───────┘ └───────┘ ┴
doc └───────┘ └───────┘
502 by rw [← sign_aux_eq_sign_aux2 _ _ n (λ _ _, h₁ _),
id └───────────────────┘ ┴ └┘
src └────┘└───────────────────┘└───┘ ┴ └────┘ └────
typ └────┘└───────────────────┘└───┘┴┴ └────┘└┘└────
doc └────┘ └───┘ ┴ └────┘ └────
txt └────┘ └───┘ ┴ └────┘ └────
par └────┘ └───┘ ┴ └────┘ └────
pid └──┘ └───┘ ┴ └────┘ └────
st └──────────────────────────────────────────────┘└─
503 ← sign_aux_eq_sign_aux2 _ _ (e.trans n) (λ _ _, h₂ _)];
id └───────────────────┘ └─────┘ ┴ └┘
src ─────────┘└───────────────────┘└───┘ └─────┘┴ └┘ └────┘ └──┘
typ ─────────┘└───────────────────┘└───┘ └─────┘┴┴└┘ └────┘└┘└──┘
doc ─────────┘ └───┘ ┴ └┘ └────┘ └──┘
txt ─────────┘ └───┘ ┴ └┘ └────┘ └──┘
par ─────────┘ └───┘ ┴ └┘ └────┘ └──┘
pid ─────────┘ └───┘ ┴ └┘ └────┘ └──┘
st ────────────────────────────────────────────────────────────┘┴└─
504 exact congr_arg sign_aux (equiv.ext _ _ (λ x, by simp)))
id └───────┘ └──────┘ └───────┘
src └────┘└───────┘┴└──────┘┴ └───────┘└───┘ └──┘ ┴└──┘└┘
typ └────┘└───────┘┴└──────┘┴ └───────┘└───┘ └──┘ ┴└──┘└┘
doc └────┘ ┴ ┴ └───┘ └──┘ ┴└──┘└┘
txt └────┘ ┴ ┴ └───┘ └──┘ ┴└──┘└┘
par └────┘ ┴ ┴ └───┘ └──┘ ┴└──┘└┘
pid ┴ ┴ ┴ └───┘ └──┘ └─────┘
st ─────────────────────────────────────────────────────┘└───┘└┘
505 ht hs
id └┘ └┘
typ └┘ └┘
506
507 lemma sign_symm_trans_trans [decidable_eq β] [fintype β] (f : perm α)
id └──────────┘ ┴ └─────┘ ┴ └──┘ ┴
src └──────────┘ └─────┘ └──┘
typ └──────────┘ ┴ └─────┘ ┴ └──┘ ┴
doc └─────┘ └──┘
508 (e : α ≃ β) : sign ((e.symm.trans f).trans e) = sign f :=
id ┴ ┴ ┴ └──┘ ┴└───┘└────┘ ┴ └───┘ ┴ ┴ └──┘ ┴
src ┴ └──┘ └───┘└────┘ └───┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴└───┘└────┘ ┴ └───┘ ┴ ┴ └──┘ ┴
doc ┴ └──┘ └──┘
509 sign_aux3_symm_trans_trans f e mem_univ mem_univ
id └────────────────────────┘ ┴ ┴ └──────┘ └──────┘
src └────────────────────────┘ └──────┘ └──────┘
typ └────────────────────────┘ ┴ ┴ └──────┘ └──────┘
510
511 lemma sign_prod_list_swap {l : list (perm α)}
id └──┘ └──┘ ┴
src └──┘ └──┘
typ └──┘ └──┘ ┴
doc └──┘
512 (hl : ∀ g ∈ l, is_swap g) : sign l.prod = -1 ^ l.length :=
id ┴ ┴ └─────┘ ┴ └──┘ ┴└───┘ ┴ ┴ ┴ ┴└─────┘
src └─────┘ └──┘ └───┘ ┴ ┴ ┴ └─────┘
typ ┴ ┴ └─────┘ ┴ └──┘ ┴└───┘ ┴ ┴ ┴ ┴└─────┘
doc └──┘ └───┘
513 have h₁ : l.map sign = list.repeat (-1) l.length :=
id ┴└──┘ └──┘ ┴ └─────────┘ ┴ ┴└─────┘
src └──┘ └──┘ ┴ └─────────┘ ┴ └─────┘
typ ┴└──┘ └──┘ ┴ └─────────┘ ┴ ┴└─────┘
doc └──┘
514 list.eq_repeat.2 ⟨by simp, λ u hu,
id └────────────┘┴ ┴ └┘
src └────────────┘┴ └──┘
typ └────────────┘┴ └──┘ ┴ └┘
doc └──┘
txt └──┘
par └──┘
st └───┘
515 let ⟨g, hg⟩ := list.mem_map.1 hu in
id └─┘ └┘ └──────────┘┴ └┘
src └──────────┘┴
typ └─┘ └┘ └──────────┘┴ └┘
516 hg.2 ▸ sign_eq_of_is_swap (hl _ hg.1)⟩,
id ┴ ┴ └────────────────┘ └┘ ┴
src ┴ ┴ └────────────────┘ ┴
typ ┴ ┴ └────────────────┘ └┘ ┴
517 by rw [← list.prod_repeat, ← h₁, list.prod_hom _ (@sign α _ _)]
id └──────────────┘ └┘ └───────────┘ └──┘ ┴
src └────┘└──────────────┘└──┘ └┘└───────────┘└─┘ └──┘┴ └──────
typ └────┘└──────────────┘└──┘└┘└┘└───────────┘└─┘ └──┘┴┴└──────
doc └────┘ └──┘ └┘ └─┘ └──┘┴ └──────
txt └────┘ └──┘ └┘ └─┘ ┴ └──────
par └────┘ └──┘ └┘ └─┘ ┴ └──────
pid └──┘ └──┘ └┘ └─┘ ┴ └────┘└
st └─────────────────────┘└────┘└─────────────────────────────┘┴└
518
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
519 lemma sign_surjective (hα : 1 < fintype.card α) : function.surjective (sign : perm α → units ℤ) :=
id ┴ └──────────┘ ┴ └─────────────────┘ └──┘ └──┘ ┴ └───┘ ┴
src ┴ └──────────┘ └─────────────────┘ └──┘ └──┘ └───┘ ┴
typ ┴ └──────────┘ ┴ └─────────────────┘ └──┘ └──┘ ┴ └───┘ ┴
doc └──────────┘ └──┘ └──┘
520 λ a, (int.units_eq_one_or a).elim
id ┴ └─────────────────┘ ┴ └──┘
src └─────────────────┘ └──┘
typ ┴ └─────────────────┘ ┴ └──┘
521 (λ h, ⟨1, by simp [h]⟩)
id ┴ ┴
src └────┘ ┴
typ ┴ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
522 (λ h, let ⟨x⟩ := fintype.card_pos_iff.1 (lt_trans zero_lt_one hα) in
id ┴ └─┘ ┴ └──────────────────┘┴ └──────┘ └─────────┘ └┘
src └──────────────────┘┴ └──────┘ └─────────┘
typ ┴ └─┘ ┴ └──────────────────┘┴ └──────┘ └─────────┘ └┘
523 let ⟨y, hxy⟩ := fintype.exists_ne_of_one_lt_card hα x in
id └─┘ ┴ └──────────────────────────────┘ └┘
src └──────────────────────────────┘
typ └─┘ ┴ └──────────────────────────────┘ └┘
524 ⟨swap y x, by rw [sign_swap hxy, h]⟩ )
id └──┘ └───────┘ └─┘ ┴
src └──┘ └──┘└───────┘┴ └┘ ┴
typ └──┘ └──┘└───────┘┴└─┘└┘┴┴
doc └──┘ └──┘ ┴ └┘ ┴
txt └──┘ ┴ └┘ ┴
par └──┘ ┴ └┘ ┴
pid └┘ ┴ └┘ ┴
st └────────────────┘└─┘┴
525
526 lemma eq_sign_of_surjective_hom {s : perm α → units ℤ}
id └──┘ ┴ └───┘ ┴
src └──┘ └───┘ ┴
typ └──┘ ┴ └───┘ ┴
doc └──┘
527 [is_group_hom s] (hs : surjective s) : s = sign :=
id └──────────┘ ┴ └────────┘ ┴ ┴ ┴ └──┘
src └──────────┘ └────────┘ ┴ └──┘
typ └──────────┘ ┴ └────────┘ ┴ ┴ ┴ └──┘
doc └──────────┘ └──┘
528 have ∀ {f}, is_swap f → s f = -1 :=
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
529 λ f ⟨x, y, hxy, hxy'⟩, hxy'.symm ▸ by_contradiction (λ h,
id ┴ ┴ └──┘ └───┘ ┴ └──────────────┘ ┴
src └───┘ ┴ └──────────────┘
typ ┴ ┴ └──┘ └───┘ ┴ └──────────────┘ ┴
530 have ∀ f, is_swap f → s f = 1 := λ f ⟨a, b, hab, hab'⟩,
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
531 by rw [← is_conj_iff_eq, ← or.resolve_right (int.units_eq_one_or _) h, hab'];
id └────────────┘ └──────────────┘ └─────────────────┘ ┴ └──┘
src └────┘└────────────┘└──┘└──────────────┘┴ └─────────────────┘└──┘ └┘ ┴
typ └────┘└────────────┘└──┘└──────────────┘┴ └─────────────────┘└──┘┴└┘└──┘┴
doc └────┘ └──┘ ┴ └──┘ └┘ ┴
txt └────┘ └──┘ ┴ └──┘ └┘ ┴
par └────┘ └──┘ ┴ └──┘ └┘ ┴
pid └──┘ └──┘ ┴ └──┘ └┘ ┴
st └───────────────────┘└────────────────────────────────────────────┘└────┘┴└─
532 exact is_group_hom.is_conj _ (is_conj_swap hab hxy),
id └──────────────────┘ └──────────┘ └─┘ └─┘
src └────┘└──────────────────┘└─┘ └──────────┘┴ ┴ ┴
typ └────┘└──────────────────┘└─┘ └──────────┘┴└─┘┴└─┘┴
doc └────┘ └─┘ ┴ ┴ ┴
txt └────┘ └─┘ ┴ ┴ ┴
par └────┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘
533 let ⟨g, hg⟩ := hs (-1) in
id └─┘ ┴ └┘ ┴
src ┴
typ └─┘ ┴ └┘ ┴
534 let ⟨l, hl⟩ := trunc.out (trunc_swap_factors g) in
id └─┘ ┴ └┘ └───────┘ └────────────────┘
src └───────┘ └────────────────┘
typ └─┘ ┴ └┘ └───────┘ └────────────────┘
doc └───────┘
535 have ∀ a ∈ l.map s, a = (1 : units ℤ) := λ a ha,
id ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘
src └──┘ ┴ └───┘ ┴
typ ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘
536 let ⟨g, hg⟩ := list.mem_map.1 ha in hg.2 ▸ this _ (hl.2 _ hg.1),
id └─┘ └┘ └──────────┘┴ └┘ ┴ ┴ └──┘ ┴ ┴
src └──────────┘┴ ┴ ┴ ┴ ┴
typ └─┘ └┘ └──────────┘┴ └┘ ┴ ┴ └──┘ ┴ ┴
537 have s l.prod = 1,
id ┴ └───┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴
doc └───┘
538 by rw [← l.prod_hom s, list.eq_repeat'.2 this, list.prod_repeat, one_pow],
id └────────┘ ┴ └─────────────┘ └──┘ └──────────────┘ └─────┘
src └────┘└────────┘┴ └┘└─────────────┘└─┘ └┘└──────────────┘└┘└─────┘┴
typ └────┘└────────┘┴┴└┘└─────────────┘└─┘└──┘└┘└──────────────┘└┘└─────┘┴
doc └────┘ ┴ └┘ └─┘ └┘ └┘ ┴
txt └────┘ ┴ └┘ └─┘ └┘ └┘ ┴
par └────┘ ┴ └┘ └─┘ └┘ └┘ ┴
pid └──┘ ┴ └┘ └─┘ └┘ └┘ ┴
st └─────────────────┘└──────────────────────┘└────────────────┘└───────┘┴
539 by rw [hl.1, hg] at this;
id └┘ └┘
src └──┘ └──┘ └───────┘
typ └──┘└┘└──┘└┘└───────┘
doc └──┘ └──┘ └───────┘
txt └──┘ └──┘ └───────┘
par └──┘ └──┘ └───────┘
pid └┘ └──┘ ┴└──────┘
st └─────┘└────┘┴└─────────
540 exact absurd this dec_trivial),
id └────┘ └──┘ └─────────┘
src └────┘└────┘┴ ┴└─────────┘
typ └────┘└────┘┴└──┘┴└─────────┘
doc └────┘ ┴ ┴└─────────┘
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────┘
541 funext $ λ f,
id └────┘ ┴
src └────┘
typ └────┘ ┴
542 let ⟨l, hl₁, hl₂⟩ := trunc.out (trunc_swap_factors f) in
id └─┘ ┴ └─┘ └───────┘ └────────────────┘ ┴
src └───────┘ └────────────────┘
typ └─┘ ┴ └─┘ └───────┘ └────────────────┘ ┴
doc └───────┘
543 have hsl : ∀ a ∈ l.map s, a = (-1 : units ℤ) := λ a ha,
id ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘
src └──┘ ┴ ┴ └───┘ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └┘
544 let ⟨g, hg⟩ := list.mem_map.1 ha in hg.2 ▸ this (hl₂ _ hg.1),
id └─┘ └┘ └──────────┘┴ └┘ ┴ ┴ └──┘ ┴
src └──────────┘┴ ┴ ┴ ┴
typ └─┘ └┘ └──────────┘┴ └┘ ┴ ┴ └──┘ ┴
545 by rw [← hl₁, ← l.prod_hom s, list.eq_repeat'.2 hsl, list.length_map,
id └─┘ └────────┘ ┴ └─────────────┘ └─┘ └─────────────┘
src └────┘ └──┘└────────┘┴ └┘└─────────────┘└─┘ └┘└─────────────┘└─
typ └────┘└─┘└──┘└────────┘┴┴└┘└─────────────┘└─┘└─┘└┘└─────────────┘└─
doc └────┘ └──┘ ┴ └┘ └─┘ └┘ └─
txt └────┘ └──┘ ┴ └┘ └─┘ └┘ └─
par └────┘ └──┘ ┴ └┘ └─┘ └┘ └─
pid └──┘ └──┘ ┴ └┘ └─┘ └┘ └─
st └────────┘└──────────────┘└─────────────────────┘└───────────────┘└─
546 list.prod_repeat, sign_prod_list_swap hl₂]
id └──────────────┘ └─────────────────┘ └─┘
src ────┘└──────────────┘└┘└─────────────────┘┴ └─
typ ────┘└──────────────┘└┘└─────────────────┘┴└─┘└─
doc ────┘ └┘ ┴ └─
txt ────┘ └┘ ┴ └─
par ────┘ └┘ ┴ └─
pid ────┘ └┘ ┴ ┴└
st ────────────────────┘└───────────────────────┘┴└
547
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
548 lemma sign_subtype_perm (f : perm α) {p : α → Prop} [decidable_pred p]
id └──┘ ┴ ┴ └────────────┘ ┴
src └──┘ └────────────┘
typ └──┘ ┴ ┴ └────────────┘ ┴
doc └──┘
549 (h₁ : ∀ x, p x ↔ p (f x)) (h₂ : ∀ x, f x ≠ x → p x) : sign (subtype_perm f h₁) = sign f :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────────┘ ┴ └┘ ┴ └──┘ ┴
src ┴ ┴ └──┘ └──────────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────────┘ ┴ └┘ ┴ └──┘ ┴
doc └──┘ └──┘
550 let l := trunc.out (trunc_swap_factors (subtype_perm f h₁)) in
id ┴ └───────┘ └────────────────┘ └──────────┘ ┴ └┘
src └───────┘ └────────────────┘ └──────────┘
typ ┴ └───────┘ └────────────────┘ └──────────┘ ┴ └┘
doc └───────┘
551 have hl' : ∀ g' ∈ l.1.map of_subtype, is_swap g' :=
id └┘ ┴┴ └─┘ └────────┘ └─────┘ └┘
src ┴ └─┘ └────────┘ └─────┘
typ └┘ ┴┴ └─┘ └────────┘ └─────┘ └┘
552 λ g' hg',
id └┘ └─┘
typ └┘ └─┘
553 let ⟨g, hg⟩ := list.mem_map.1 hg' in
id └─┘ └┘ └──────────┘┴ └─┘
src └──────────┘┴
typ └─┘ └┘ └──────────┘┴ └─┘
554 hg.2 ▸ is_swap_of_subtype (l.2.2 _ hg.1),
id ┴ ┴ └────────────────┘ ┴┴ ┴ ┴
src ┴ ┴ └────────────────┘ ┴ ┴ ┴
typ ┴ ┴ └────────────────┘ ┴┴ ┴ ┴
555 have hl'₂ : (l.1.map of_subtype).prod = f,
id ┴┴ └─┘ └────────┘ └──┘ ┴ ┴
src ┴ └─┘ └────────┘ └──┘ ┴
typ ┴┴ └─┘ └────────┘ └──┘ ┴ ┴
doc └──┘
556 by rw [l.1.prod_hom of_subtype, l.2.1, of_subtype_subtype_perm _ h₂],
id ┴ └────────┘ ┴ └─────────────────────┘ └┘
src └──┘ └──────────┘└────────┘└┘ └────┘└─────────────────────┘└─┘ ┴
typ └──┘┴└──────────┘└────────┘└┘┴└────┘└─────────────────────┘└─┘└┘┴
doc └──┘ └──────────┘ └┘ └────┘ └─┘ ┴
txt └──┘ └──────────┘ └┘ └────┘ └─┘ ┴
par └──┘ └──────────┘ └┘ └────┘ └─┘ ┴
pid └┘ └──────────┘ └┘ └────┘ └─┘ ┴
st └──────────────────────────┘└───┘└──────────────────────────────┘┴
557 by conv {congr, rw ← l.2.1, skip, rw ← hl'₂};
id ┴ └──┘
src └────┘└───┘└┘└───┘ └──┘└┘└──┘└┘└───┘ ┴
typ └────┘└───┘└┘└───┘┴└──┘└┘└──┘└┘└───┘└──┘┴
txt └────┘└───┘└┘└───┘ └──┘└┘└──┘└┘└───┘ ┴
par └────┘└───┘└┘└───┘ └──┘└┘└──┘└┘└───┘ ┴
pid ┴└───────────┘ └───────────────┘ ┴
st └─────┘└───┘└──────────┘└────┘└─────────┘└┘└
558 rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', list.length_map]
id └─────────────────┘ ┴ └─────────────────┘ └─┘ └─────────────┘
src └──┘└─────────────────┘┴ └────┘└─────────────────┘┴ └┘└─────────────┘└─
typ └──┘└─────────────────┘┴┴└────┘└─────────────────┘┴└─┘└┘└─────────────┘└─
doc └──┘ ┴ └────┘ ┴ └┘ └─
txt └──┘ ┴ └────┘ ┴ └┘ └─
par └──┘ ┴ └────┘ ┴ └┘ └─
pid └┘ ┴ └────┘ ┴ └┘ ┴└
st ─────┘└─────────────────────┘└─────────────────────────┘└───────────────┘┴└
559
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
560 @[simp] lemma sign_of_subtype {p : α → Prop} [decidable_pred p]
id ┴ └────────────┘ ┴
src └────────────┘
typ ┴ └────────────┘ ┴
doc └──┘
561 (f : perm (subtype p)) : sign (of_subtype f) = sign f :=
id └──┘ └─────┘ ┴ └──┘ └────────┘ ┴ ┴ └──┘ ┴
src └──┘ └─────┘ └──┘ └────────┘ ┴ └──┘
typ └──┘ └─────┘ ┴ └──┘ └────────┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘
562 have ∀ x, of_subtype f x ≠ x → p x, from λ x, not_imp_comm.1 (of_subtype_apply_of_not_mem f),
id ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘┴ └─────────────────────────┘ ┴
src └────────┘ ┴ └──────────┘┴ └─────────────────────────┘
typ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘┴ └─────────────────────────┘ ┴
563 by conv {to_rhs, rw [← subtype_perm_of_subtype f, sign_subtype_perm _ _ this]}
id └─────────────────────┘ ┴ └───────────────┘ └──┘
src └────┘└────┘└┘└────┘└─────────────────────┘┴ └┘└───────────────┘└───┘ ┴└─
typ └────┘└────┘└┘└────┘└─────────────────────┘┴┴└┘└───────────────┘└───┘└──┘┴└─
txt └────┘└────┘└┘└────┘ ┴ └┘ └───┘ ┴└─
par └────┘└────┘└┘└────┘ ┴ └┘ └───┘ ┴└─
pid ┴└─────────────┘ ┴ └┘ └───┘ └┘└
st └─────┘└────┘└───────────────────────────────┘└──────────────────────────┘ ┴└
564
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
565 lemma sign_eq_sign_of_equiv [decidable_eq β] [fintype β] (f : perm α) (g : perm β)
id └──────────┘ ┴ └─────┘ ┴ └──┘ ┴ └──┘ ┴
src └──────────┘ └─────┘ └──┘ └──┘
typ └──────────┘ ┴ └─────┘ ┴ └──┘ ┴ └──┘ ┴
doc └─────┘ └──┘ └──┘
566 (e : α ≃ β) (h : ∀ x, e (f x) = g (e x)) : sign f = sign g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc ┴ └──┘ └──┘
567 have hg : g = (e.symm.trans f).trans e, from equiv.ext _ _ $ by simp [h],
id ┴ ┴ ┴└───┘└────┘ ┴ └───┘ ┴ └───────┘ ┴
src ┴ └───┘└────┘ └───┘ └───────┘ └────┘ ┴
typ ┴ ┴ ┴└───┘└────┘ ┴ └───┘ ┴ └───────┘ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
568 by rw [hg, sign_symm_trans_trans]
id └┘ └───────────────────┘
src └──┘ └┘└───────────────────┘└─
typ └──┘└┘└┘└───────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────┘└─────────────────────┘┴└
569
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
570 lemma sign_bij [decidable_eq β] [fintype β]
id └──────────┘ ┴ └─────┘ ┴
src └──────────┘ └─────┘
typ └──────────┘ ┴ └─────┘ ┴
doc └─────┘
571 {f : perm α} {g : perm β} (i : Π x : α, f x ≠ x → β)
id └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
572 (h : ∀ x hx hx', i (f x) hx' = g (i x hx))
id ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
src ┴
typ ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
573 (hi : ∀ x₁ x₂ hx₁ hx₂, i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂)
id └┘ └┘ └─┘ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └─┘ └┘ ┴ └┘
src ┴ ┴
typ └┘ └┘ └─┘ └─┘ ┴ └┘ └─┘ ┴ ┴ └┘ └─┘ └┘ ┴ └┘
574 (hg : ∀ y, g y ≠ y → ∃ x hx, i x hx = y) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴ └┘ ┴ ┴
575 sign f = sign g :=
id └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
576 calc sign f = sign (@subtype_perm _ f (λ x, f x ≠ x) (by simp)) :
id └──┘ ┴ └──┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ └──────────┘ ┴ └──┘
typ └──┘ ┴ └──┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘ └──┘ └──┘
txt └──┘
par └──┘
st └───┘
577 eq.symm (sign_subtype_perm _ _ (λ _, id))
id └─────┘ └───────────────┘ ┴ └┘
src └─────┘ └───────────────┘ └┘
typ └─────┘ └───────────────┘ ┴ └┘
578 ... = sign (@subtype_perm _ g (λ x, g x ≠ x) (by simp)) :
id └──┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──────────┘ ┴ └──┘
typ └──┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
txt └──┘
par └──┘
st └───┘
579 sign_eq_sign_of_equiv _ _
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
580 (equiv.of_bijective
id └────────────────┘
src └────────────────┘
typ └────────────────┘
581 (show function.bijective (λ x : {x // f x ≠ x},
id └────────────────┘ ┴┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ ┴┴ ┴ ┴ ┴ ┴
582 (⟨i x.1 x.2, have f (f x) ≠ f x, from mt (λ h, f.injective h) x.2,
id ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└────────┘ ┴ ┴┴
src ┴ ┴ ┴ └┘ └────────┘ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└────────┘ ┴ ┴┴
583 by rw [← h _ x.2 this]; exact mt (hi _ _ this x.2) x.2⟩ : {y // g y ≠ y})),
id ┴ ┴ └──┘ └┘ └┘ └──┘ ┴ ┴┴ ┴ ┴ ┴ ┴
src └────┘ └─┘ └─┘ ┴ └────┘└┘┴ └───┘ ┴ └──┘ └┘ ┴ ┴
typ └────┘┴└─┘┴└─┘└──┘┴ └────┘└┘┴ └┘└───┘└──┘┴ └──┘┴└┘ ┴┴ ┴ ┴ ┴ ┴
doc └────┘ └─┘ └─┘ ┴ └────┘ ┴ └───┘ ┴ └──┘ └┘
txt └────┘ └─┘ └─┘ ┴ └────┘ ┴ └───┘ ┴ └──┘ └┘
par └────┘ └─┘ └─┘ ┴ └────┘ ┴ └───┘ ┴ └──┘ └┘
pid └──┘ └─┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └──┘ └┘
st └─────────────────┘┴└──────────────────────────────┘
584 from ⟨λ ⟨x, hx⟩ ⟨y, hy⟩ h, subtype.eq (hi _ _ _ _ (subtype.mk.inj h)),
id ┴ ┴ ┴ └────────┘ └┘ └────────────┘ ┴
src └────────┘ └────────────┘
typ ┴ ┴ ┴ └────────┘ └┘ └────────────┘ ┴
585 λ ⟨y, hy⟩, let ⟨x, hfx, hx⟩ := hg y hy in ⟨⟨x, hfx⟩, subtype.eq hx⟩⟩))
id ┴┴ └┘ └─┘ ┴ └─┘ └┘ └┘ └────────┘
src └────────┘
typ ┴┴ └┘ └─┘ ┴ └─┘ └┘ └┘ └────────┘
586 (λ ⟨x, _⟩, subtype.eq (h x _ _))
id ┴┴ └────────┘ ┴
src └────────┘
typ ┴┴ └────────┘ ┴
587 ... = sign g : sign_subtype_perm _ _ (λ _, id)
id └──┘ ┴ └───────────────┘ ┴ └┘
src └──┘ └───────────────┘ └┘
typ └──┘ ┴ └───────────────┘ ┴ └┘
doc └──┘
588
589 def is_cycle (f : perm β) := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
id └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
typ └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
590
591 lemma is_cycle_swap {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
id ┴ ┴ ┴ ┴ └──────┘ └──┘ ┴ ┴
src ┴ └──────┘ └──┘
typ ┴ ┴ ┴ ┴ └──────┘ └──┘ ┴ ┴
doc └──┘
592 ⟨y, by rwa swap_apply_right,
id ┴ └──────────────┘
src └──┘└──────────────┘
typ ┴ └──┘└──────────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
593 λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
594 if hya : y = a then ⟨0, hya⟩
id └┘ ┴ ┴ ┴ └─┘
src └┘ ┴
typ └┘ ┴ ┴ ┴ └─┘
595 else ⟨1, by rw [gpow_one, swap_apply_def]; split_ifs at *; cc⟩⟩
id ┴ └──────┘ └────────────┘
src └──┘└──────┘└┘└────────────┘┴ └────────────┘ └┘
typ ┴ └──┘└──────┘└┘└────────────┘┴ └────────────┘ └┘
doc └──┘ └┘ ┴ └────────────┘ └┘
txt └──┘ └┘ ┴ └────────────┘ └┘
par └──┘ └┘ ┴ └────────────┘ └┘
pid └┘ └┘ ┴ └───┘
st └───────────┘└──────────────┘┴└──────────────────┘
596
597 lemma is_cycle_inv {f : perm β} (hf : is_cycle f) : is_cycle (f⁻¹) :=
id └──┘ ┴ └──────┘ ┴ └──────┘ ┴└┘
src └──┘ └──────┘ └──────┘ └┘
typ └──┘ ┴ └──────┘ ┴ └──────┘ ┴└┘
doc └──┘
598 let ⟨x, hx⟩ := hf in
id └─┘ ┴ └┘ └┘
typ └─┘ ┴ └┘ └┘
599 ⟨x, by simp [eq_inv_iff_eq, inv_eq_iff_eq, *] at *; cc,
id └───────────┘ └───────────┘
src └────┘└───────────┘└┘└───────────┘└───────┘ └┘
typ └────┘└───────────┘└┘└───────────┘└───────┘ └┘
doc └────┘ └┘ └───────┘ └┘
txt └────┘ └┘ └───────┘ └┘
par └────┘ └┘ └───────┘ └┘
pid ┴┴ └┘ └──┘┴└──┘
st └──────────────────────────────────────────────┘
600 λ y hy, let ⟨i, hi⟩ := hx.2 y (by simp [eq_inv_iff_eq, inv_eq_iff_eq, *] at *; cc) in
id ┴ └┘ └─┘ ┴ ┴ ┴ └───────────┘ └───────────┘
src ┴ └────┘└───────────┘└┘└───────────┘└───────┘ └┘
typ ┴ └┘ └─┘ ┴ ┴ ┴ └────┘└───────────┘└┘└───────────┘└───────┘ └┘
doc └────┘ └┘ └───────┘ └┘
txt └────┘ └┘ └───────┘ └┘
par └────┘ └┘ └───────┘ └┘
pid ┴┴ └┘ └──┘┴└──┘
st └──────────────────────────────────────────────┘
601 ⟨-i, by rwa [gpow_neg, inv_gpow, inv_inv]⟩⟩
id ┴ └──────┘ └──────┘ └─────┘
src ┴ └───┘└──────┘└┘└──────┘└┘└─────┘┴
typ ┴ └───┘└──────┘└┘└──────┘└┘└─────┘┴
doc └───┘ └┘ └┘ ┴
txt └───┘ └┘ └┘ ┴
par └───┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └────────────┘└────────┘└───────┘┴
602
603 lemma exists_gpow_eq_of_is_cycle {f : perm β} (hf : is_cycle f) {x y : β}
id └──┘ ┴ └──────┘ ┴ ┴
src └──┘ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴
doc └──┘
604 (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℤ, (f ^ i) x = y :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
605 let ⟨g, hg⟩ := hf in
id └─┘ └┘ └┘
typ └─┘ └┘ └┘
606 let ⟨a, ha⟩ := hg.2 x hx in
id └─┘ ┴ ┴ ┴ └┘
src ┴
typ └─┘ ┴ ┴ ┴ └┘
607 let ⟨b, hb⟩ := hg.2 y hy in
id └─┘ ┴ ┴ ┴ └┘
src ┴
typ └─┘ ┴ ┴ ┴ └┘
608 ⟨b - a, by rw [← ha, ← mul_apply, ← gpow_add, sub_add_cancel, hb]⟩
id ┴ └┘ └───────┘ └──────┘ └────────────┘ └┘
src ┴ └────┘ └──┘└───────┘└──┘└──────┘└┘└────────────┘└┘ ┴
typ ┴ └────┘└┘└──┘└───────┘└──┘└──────┘└┘└────────────┘└┘└┘┴
doc └────┘ └──┘ └──┘ └┘ └┘ ┴
txt └────┘ └──┘ └──┘ └┘ └┘ ┴
par └────┘ └──┘ └──┘ └┘ └┘ ┴
pid └──┘ └──┘ └──┘ └┘ └┘ ┴
st └───────┘└───────────┘└──────────┘└──────────────┘└──┘┴
609
610 lemma is_cycle_swap_mul_aux₁ : ∀ (n : ℕ) {b x : α} {f : perm α}
id ┴ ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴
doc └──┘
611 (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
612 ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
id ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ └──┘ ┴ ┴ ┴
typ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
613 | 0 := λ b x f hb h, ⟨0, h⟩
id ┴ ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴
614 | (n+1 : ℕ) := λ b x f hb h,
id ┴┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ └┘ ┴
615 if hfbx : f x = b then ⟨0, hfbx⟩
id └┘ ┴ ┴ ┴ ┴ └──┘
src └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ └──┘
616 else
617 have f b ≠ b ∧ b ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hb,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────────────┘ └┘
src ┴ ┴ ┴ └─────────────────────────────────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────────────┘ └┘
618 have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴
src └──┘ ┴ └┘ ┴ └┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴
doc └──┘
619 by rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx),
id └───────┘ └────────────┘ └────────────────────┘ └──┘ └─────┘ └──┘
src └──┘└───────┘└┘└────────────┘└┘└────────────────────┘┴ └─┘ └─────┘┴ └──
typ └──┘└───────┘└┘└────────────┘└┘└────────────────────┘┴└──┘└─┘ └─────┘┴└──┘└──
doc └──┘ └┘ └┘ ┴ └─┘ ┴ └──
txt └──┘ └┘ └┘ ┴ └─┘ ┴ └──
par └──┘ └┘ └┘ ┴ └─┘ ┴ └──
pid └┘ └┘ └┘ ┴ └─┘ ┴ └──
st └────────────┘└──────────────┘└────────────────────────────────────────────┘└─
620 ne.def, ← injective.eq_iff f.injective, apply_inv_self];
id └────┘ └──────────────┘ └─────────┘ └────────────┘
src ─────────┘└────┘└──┘└──────────────┘┴└─────────┘└┘└────────────┘┴
typ ─────────┘└────┘└──┘└──────────────┘┴└─────────┘└┘└────────────┘┴
doc ─────────┘ └──┘ ┴ └┘ ┴
txt ─────────┘ └──┘ ┴ └┘ ┴
par ─────────┘ └──┘ ┴ └┘ ┴
pid ─────────┘ └──┘ ┴ └┘ ┴
st ───────────────┘└──────────────────────────────┘└──────────────┘┴└─
621 exact this.1,
id └──┘
src └────┘ └┘
typ └────┘└──┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ───────────────────┘
622 let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb'
id └─┘ ┴ └────────────────────┘ └─┘
typ └─┘ ┴ └────────────────────┘ └─┘
623 (f.injective $
id ┴└────────┘
src └────────┘
typ ┴└────────┘
624 by rw [apply_inv_self];
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └─────────────────┘┴└─
625 rwa [pow_succ, mul_apply] at h) in
id └──────┘ └───────┘
src └───┘└──────┘└┘└───────┘└────┘
typ └───┘└──────┘└┘└───────┘└────┘
doc └───┘ └┘ └────┘
txt └───┘ └┘ └────┘
par └───┘ └┘ └────┘
pid └┘ └┘ ┴└───┘
st ────────────┘└──────┘└─────────┘┴└───┘
626 ⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
id ┴ └──────┘ └──────┘ └───────┘ └┘ └──────┘ └───────┘ └────────────┘
src ┴ └──┘└──────┘└┘└──────┘└┘└───────┘└┘ └┘└──────┘└┘└───────┘└┘└────────────┘└─
typ ┴ └──┘└──────┘└┘└──────┘└┘└───────┘└┘└┘└┘└──────┘└┘└───────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
st └───────────┘└────────┘└─────────┘└──┘└────────┘└─────────┘└──────────────┘└─
627 swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (ne.symm hfbx)]⟩
id └────────────────────┘ └─────────────────────────────────┘ └┘ └─────┘ └──┘
src ───────┘└────────────────────┘┴ └─────────────────────────────────┘┴ └──┘ └─────┘┴ └┘
typ ───────┘└────────────────────┘┴ └─────────────────────────────────┘┴└┘└──┘ └─────┘┴└──┘└┘
doc ───────┘ ┴ ┴ └──┘ ┴ └┘
txt ───────┘ ┴ ┴ └──┘ ┴ └┘
par ───────┘ ┴ ┴ └──┘ ┴ └┘
pid ───────┘ ┴ ┴ └──┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────┘┴
628
629 lemma is_cycle_swap_mul_aux₂ : ∀ (n : ℤ) {b x : α} {f : perm α}
id ┴ ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴
doc └──┘
630 (hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
631 ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
id ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ └──┘ ┴ ┴ ┴
typ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
632 | (n : ℕ) := λ b x f, is_cycle_swap_mul_aux₁ n
id ┴ ┴ ┴ ┴ ┴ └────────────────────┘
src ┴ └────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────────────────┘
633 | -[1+ n] := λ b x f hb h,
id └──┘ ┴┴ ┴ ┴ ┴ └┘ ┴
src └──┘ ┴
typ └──┘ ┴┴ ┴ ┴ ┴ └┘ ┴
634 if hfbx : f⁻¹ x = b then ⟨-1, by rwa [gpow_neg, gpow_one, mul_inv_rev, mul_apply, swap_inv, swap_apply_right]⟩
id └┘ ┴└┘ ┴ ┴ ┴ ┴ └──────┘ └──────┘ └─────────┘ └───────┘ └──────┘ └──────────────┘
src └┘ └┘ ┴ ┴ └───┘└──────┘└┘└──────┘└┘└─────────┘└┘└───────┘└┘└──────┘└┘└──────────────┘┴
typ └┘ ┴└┘ ┴ ┴ ┴ ┴ └───┘└──────┘└┘└──────┘└┘└─────────┘└┘└───────┘└┘└──────┘└┘└──────────────┘┴
doc └───┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └───┘ └┘ └┘ └┘ └┘ └┘ ┴
par └───┘ └┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ └┘ ┴
st └────────────┘└────────┘└───────────┘└─────────┘└────────┘└────────────────┘┴
635 else if hfbx' : f x = b then ⟨0, hfbx'⟩
id └┘ ┴ ┴ ┴ ┴ └───┘
src └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ └───┘
636 else
637 have f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────────────┘ └┘
src ┴ ┴ ┴ └─────────────────────────────────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────────────────┘ └┘
638 have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b,
id └──┘ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴└┘ ┴ ┴ ┴└┘ ┴
src └──┘ └┘ ┴ └┘ └┘ ┴ └┘
typ └──┘ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴└┘ ┴ ┴ ┴└┘ ┴
doc └──┘
639 by rw [mul_apply, swap_apply_def];
id └───────┘ └────────────┘
src └──┘└───────┘└┘└────────────┘┴
typ └──┘└───────┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────┘└──────────────┘┴└─
640 split_ifs;
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ─────────────────
641 simp [inv_eq_iff_eq, eq_inv_iff_eq] at *; cc,
id └───────────┘ └───────────┘
src └────┘└───────────┘└┘└───────────┘└────┘ └┘
typ └────┘└───────────┘└┘└───────────┘└────┘ └┘
doc └────┘ └┘ └────┘ └┘
txt └────┘ └┘ └────┘ └┘
par └────┘ └┘ └────┘ └┘
pid ┴┴ └┘ ┴┴└──┘
st ─────────────────────────────────────────────────┘
642 let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb
id └─┘ ┴ └────────────────────┘ └┘
src └────────────────────┘
typ └─┘ ┴ └────────────────────┘ └┘
643 (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b, by
id ┴└┘ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴
src └┘ ┴ └┘ ┴ └┘
typ ┴└┘ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴
st └
644 rw [← gpow_coe_nat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, gpow_neg_succ, ← inv_pow, pow_succ', mul_assoc,
id └──────────┘ ┴ └───────┘ └───────┘ └───────┘ └───────────┘ └─────┘ └───────┘ └───────┘
src └────┘└──────────┘└──┘ └──┘└───────┘└──┘└───────┘└──┘└───────┘└┘└───────────┘└──┘└─────┘└┘└───────┘└┘└───────┘└─
typ └────┘└──────────┘└──┘┴└──┘└───────┘└──┘└───────┘└──┘└───────┘└┘└───────────┘└──┘└─────┘└┘└───────┘└┘└───────┘└─
doc └────┘ └──┘ └──┘ └──┘ └──┘ └┘ └──┘ └┘ └┘ └─
txt └────┘ └──┘ └──┘ └──┘ └──┘ └┘ └──┘ └┘ └┘ └─
par └────┘ └──┘ └──┘ └──┘ └──┘ └┘ └──┘ └┘ └┘ └─
pid └──┘ └──┘ └──┘ └──┘ └──┘ └┘ └──┘ └┘ └┘ └─
st ───────────────────────┘└───┘└───────────┘└───────────┘└───────────┘└─────────────┘└─────────┘└─────────┘└─────────┘└─
645 mul_assoc, inv_mul_self, mul_one, gpow_coe_nat, ← pow_succ', ← pow_succ]) in
id └───────┘ └──────────┘ └─────┘ └──────────┘ └───────┘ └──────┘
src ───────┘└───────┘└┘└──────────┘└┘└─────┘└┘└──────────┘└──┘└───────┘└──┘└──────┘┴
typ ───────┘└───────┘└┘└──────────┘└┘└─────┘└┘└──────────┘└──┘└───────┘└──┘└──────┘┴
doc ───────┘ └┘ └┘ └┘ └──┘ └──┘ ┴
txt ───────┘ └┘ └┘ └┘ └──┘ └──┘ ┴
par ───────┘ └┘ └┘ └┘ └──┘ └──┘ ┴
pid ───────┘ └┘ └┘ └┘ └──┘ └──┘ ┴
st ────────────────┘└────────────┘└───────┘└────────────┘└───────────┘└──────────┘┴
646 have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x, by rw [mul_apply, inv_apply_self, swap_apply_left],
id └──┘ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘ ┴ └───────┘ └────────────┘ └─────────────┘
src └──┘ └┘ ┴ └┘ ┴ └┘ └──┘└───────┘└┘└────────────┘└┘└─────────────┘┴
typ └──┘ ┴ ┴└┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘ ┴ └──┘└───────┘└┘└────────────┘└┘└─────────────┘┴
doc └──┘ └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └────────────┘└──────────────┘└───────────────┘┴
647 ⟨-i, by rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, gpow_add, gpow_one, gpow_neg, ← inv_gpow,
id ┴ └────────────┘ ┴ └─────┘ └────────────┘ └──────┘ └──────┘ └──────┘ └──────┘
src ┴ └────┘└────────────┘┴ └──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└──┘└──────┘└─
typ ┴ └────┘└────────────┘┴┴└──┘└─────┘└┘└────────────┘└┘└──────┘└┘└──────┘└┘└──────┘└──┘└──────┘└─
doc └────┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──┘ └─
txt └────┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──┘ └─
par └────┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──┘ └─
pid └──┘ ┴ └──┘ └┘ └┘ └┘ └┘ └──┘ └─
st └──────────────────────┘└────────┘└──────────────┘└────────┘└────────┘└────────┘└──────────┘└─
648 mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, gpow_add, gpow_one,
id └─────────┘ └──────┘ └──────────────────┘ └────────────┘ └───────┘ ┴ └──────┘ └──────┘
src ─────┘└─────────┘└┘└──────┘└┘└──────────────────┘└┘└────────────┘└┘└───────┘└─┘ └┘└──────┘└┘└──────┘
typ ─────┘└─────────┘└┘└──────┘└┘└──────────────────┘└┘└────────────┘└┘└───────┘└─┘┴└┘└──────┘└┘└──────┘
doc ─────┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘
txt ─────┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘
par ─────┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘
pid ─────┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘
st ────────────────┘└────────┘└────────────────────┘└──────────────┘└─────────────┘└────────┘└────────┘
649 mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx')]⟩
id ┴
src ┴┴
typ ┴┴
doc ┴
txt ┴
par ┴
pid ┴
st └┘ ┴
650
651 lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {f : perm α} (hf : is_cycle f) {x : α}
id ┴ ┴ ┴
typ ┴ ┴ ┴
652 (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
653 equiv.ext _ _ $ λ y,
id ┴
typ ┴
654 let ⟨z, hz⟩ := hf in
id └┘
typ └┘
655 let ⟨i, hi⟩ := hz.2 x hfx in
id ┴
typ ┴
656 if hyx : y = x then by simp [hyx]
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
657 else if hfyx : y = f x then by simp [hfyx, hffx]
id ┴ ┴ ┴
typ ┴ ┴ ┴
658 else begin
659 rw [swap_apply_of_ne_of_ne hyx hfyx],
id └─┘
typ └─┘
660 refine by_contradiction (λ hy, _),
661 cases hz.2 y hy with j hj,
id ┴
typ ┴
662 rw [← sub_add_cancel j i, gpow_add, mul_apply, hi] at hj,
id ┴ ┴
typ ┴ ┴
663 cases gpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji hji,
id ┴ ┴
typ ┴ ┴
664 { rw [← hj, hji] at hyx, cc },
st └┘
665 { rw [← hj, hji] at hfyx, cc }
st └┘
666 end
667
668 lemma is_cycle_swap_mul {f : perm α} (hf : is_cycle f) {x : α}
id ┴ ┴ ┴
typ ┴ ┴ ┴
669 (hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
670 ⟨f x, by simp only [swap_apply_def, mul_apply];
id ┴ ┴
typ ┴ ┴
671 split_ifs; simp [injective.eq_iff f.injective] at *; cc,
id └┘
src └┘
typ └┘
doc └┘
672 λ y hy,
id ┴
typ ┴
673 let ⟨i, hi⟩ := exists_gpow_eq_of_is_cycle hf hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1 in
id ┴ └┘
typ ┴ └┘
674 have hi : (f ^ (i - 1)) (f x) = y, from
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
675 calc (f ^ (i - 1)) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ)) x : by rw [gpow_one, mul_apply]
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴
676 ... = y : by rwa [← gpow_add, sub_add_cancel],
id ┴
typ ┴
677 is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
678
679 @[simp] lemma support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘ ┴
680 finset.ext.2 $ λ a, by simp [swap_apply_def]; split_ifs; cc
id ┴ └┘
src └┘
typ ┴ └┘
doc └┘
681
682 lemma card_support_swap [fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
683 show (swap x y).support.card = finset.card ⟨x::y::0, by simp [hxy]⟩,
id ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ └─┘
684 from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext]; cc
id └─┘ └┘
src └┘
typ └─┘ └┘
doc └┘
685
686 lemma sign_cycle [fintype α] : ∀ {f : perm α} (hf : is_cycle f),
id └──┘ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴
doc └──┘ ┴
687 sign f = -(-1 ^ f.support.card)
id ┴ ┴
typ ┴ ┴
688 | f := λ hf,
id └┘
typ └┘
689 let ⟨x, hx⟩ := hf in
id └┘
typ └┘
690 calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
691 by rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]
st ┴
692 ... = -(-1 ^ f.support.card) :
693 if h1 : f (f x) = x
694 then
695 have h : swap x (f x) * f = 1,
696 by conv in (f) {rw eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1 };
id └┘
typ └┘
697 simp [mul_def, one_def],
698 by rw [sign_mul, sign_swap hx.1.symm, h, sign_one, eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1,
id └┘
typ └┘
699 card_support_swap hx.1.symm]; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
700 else
701 have h : card (support (swap x (f x) * f)) + 1 = card (support f),
702 by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq h1,
703 card_insert_of_not_mem (not_mem_erase _ _)],
st ┴
704 have wf : card (support (swap x (f x) * f)) < card (support f),
705 from card_support_swap_mul hx.1,
706 by rw [sign_mul, sign_swap hx.1.symm, sign_cycle (is_cycle_swap_mul hf hx.1 h1), ← h];
id └┘
typ └┘
707 simp [pow_add]
708 using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
id ┴ ┴
typ ┴ ┴
709
710 end sign
711
712 end equiv.perm
713
714 lemma finset.prod_univ_perm [fintype α] [comm_monoid β] {f : α → β} (σ : perm α) :
id └┘ └─┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └─┘ └┘ └┘ └┘ ┴
typ └┘ └─┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └─┘
715 (univ : finset α).prod f = univ.prod (λ z, f (σ z)) :=
id └┘ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └┘
typ └┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘
716 eq.symm $ prod_bij (λ z _, σ z) (λ _ _, mem_univ _) (λ _ _, rfl)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
717 (λ _ _ _ _ H, σ.injective H) (λ b _, ⟨σ⁻¹ b, mem_univ _, by simp⟩)
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
718
719 lemma finset.sum_univ_perm [fintype α] [add_comm_monoid β] {f : α → β} (σ : perm α) :
id └──┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └──┘ ┴ └┘ └┘ └┘ └┘ └┘
typ └──┘ ┴ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └──┘ ┴
720 (univ : finset α).sum f = univ.sum (λ z, f (σ z)) :=
id └┘ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └┘
typ └┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘
721 @finset.prod_univ_perm _ (multiplicative β) _ _ f σ
id ┴ ┴ ┴
typ ┴ ┴ ┴
722
723 attribute [to_additive] finset.prod_univ_perm
doc ┴ └───────┘